]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_reqx.ma
update in staic_2 and basic_2
[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / rt_transition / cpx_reqx.ma
index 7c05f8b2c7307aca46ff2a1e1176fea951105032..6c1aa906b62dc015aaa18dd73827f50530d22e4f 100644 (file)
@@ -22,7 +22,7 @@ include "basic_2/rt_transition/rpx_fsle.ma".
 (* Basic_2A1: was just: cpx_lleq_conf_sn *)
 lemma cpx_reqx_conf_sn (G):
       s_r_confluent1 … (cpx G) reqx.
-/3 width=6 by cpx_rex_conf/ qed-.
+/3 width=6 by cpx_rex_conf_sn/ qed-.
 
 (* Basic_2A1: was just: cpx_lleq_conf_dx *)
 lemma cpx_reqx_conf_dx (G) (L2):