search

harp-project / AML-Formalization

GNU Lesser General Public License v2.1
10 stars 5 forks source link

Adding new theorem #419

Closed adilido99 closed 4 months ago

adilido99 commented 11 months ago

forall Γ Γ' φ i, Γ ⊆ Γ' -> Γ ⊢i φ using i -> Γ' ⊢i φ using i.