]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/basic_2/static/sta_lift.ma
some renaming and some typos corrected ...
[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / static / sta_lift.ma
index 89868cfc3d0b46fa219aaa8bc2829c440c593046..4d342878f288f27581933e980398eb50e9eea0d5 100644 (file)
@@ -94,7 +94,7 @@ lemma sta_inv_lift1: ∀h,G. l_deliftable_sn (sta h G).
 ]
 qed-.
 
-(* Advanced forvard lemmas **************************************************)
+(* Advanced forward lemmas **************************************************)
 
 (* Basic_1: was: sty0_correct *)
 lemma sta_fwd_correct: ∀h,G,L,T,U. ⦃G, L⦄ ⊢ T •[h] U → ∃T0. ⦃G, L⦄ ⊢ U •[h] T0.