]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/basic_2/computation/acp_aaa.ma
- lambdadelta: tentative definition of lazy equivalence for closures +
[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / computation / acp_aaa.ma
index e508aac3101ec992db96f9ec10adb30943e59964..13d69acd47b067ccfa9ee917b75b874c3bbc61d9 100644 (file)
@@ -20,7 +20,7 @@ include "basic_2/computation/lsubc_ldrops.ma".
 
 (* ABSTRACT COMPUTATION PROPERTIES ******************************************)
 
-(* Main propertis ***********************************************************)
+(* Main properties **********************************************************)
 
 (* Basic_1: was: sc3_arity_csubc *)
 theorem aacr_aaa_csubc_lifts: ∀RR,RS,RP.