]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/basic_2/multiple/fleq.ma
some renaming and some typos corrected ...
[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / multiple / fleq.ma
index b7120b85bb4ad1073c64deb49e0757dc5854689a..910dca14ccd2574eb5458dbc88bf85bbb9ffe989 100644 (file)
@@ -26,7 +26,7 @@ interpretation
    "lazy equivalence (closure)"
    'LazyEq d G1 L1 T1 G2 L2 T2 = (fleq d G1 L1 T1 G2 L2 T2).
 
-(* Basic_properties *********************************************************)
+(* Basic properties *********************************************************)
 
 lemma fleq_refl: ∀d. tri_reflexive … (fleq d).
 /2 width=1 by fleq_intro/ qed.