]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/lib/lambda-delta/substitution/lift_main.ma
- xoa: bug fix and improvement
[helm.git] / matita / matita / lib / lambda-delta / substitution / lift_main.ma
index a41e49c5b86eea11ab3d1d0929b7445de2f31678..5ef9a31f46cabba60ef06ed58dc84746758959d1 100644 (file)
@@ -16,7 +16,7 @@ include "lambda-delta/substitution/lift_defs.ma".
 
 (* RELOCATION ***************************************************************)
 
-(* the main properies *******************************************************)
+(* Main properies ***********************************************************)
 
 lemma lift_div_le: ∀d1,e1,T1,T. ↑[d1, e1] T1 ≡ T →
                    ∀d2,e2,T2. ↑[d2 + e1, e2] T2 ≡ T →