]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/basic_2/computation/ltprs_ltprs.ma
commit completed! some bugs fixed and some instances of auto resized
[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / computation / ltprs_ltprs.ma
index e529ee31a7fc0bc3b0959ba5ab31f6bb460f1813..aec82cd5ae1b30dcec47632d41d5ae11638fb043 100644 (file)
@@ -25,7 +25,7 @@ lemma ltprs_strip: ∀L1. ∀L:term. L ➡* L1 → ∀L2. L ➡ L2 →
 
 (* Main properties **********************************************************)
 
-theorem ltprs_conf: Confluent … ltprs.
+theorem ltprs_conf: confluent … ltprs.
 /3 width=3/ qed.
 
 theorem ltprs_trans: Transitive … ltprs.