]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/basic_2/substitution/fqup_fqup.ma
commit of the "substitution" component and of some auxiliary files ...
[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / substitution / fqup_fqup.ma
index a6bff5edee5a8bcf91122a072db40dc5763244f6..0dd0e336fb89f51a33d47fb3f06850f23b48269a 100644 (file)
@@ -16,7 +16,7 @@ include "basic_2/substitution/fqup.ma".
 
 (* PLUS-ITERATED SUPCLOSURE *************************************************)
 
-(* Main propertis ***********************************************************)
+(* Main properties **********************************************************)
 
 theorem fqup_trans: tri_transitive … fqup.
 /2 width=5 by tri_TC_transitive/ qed-.