]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_reqg.ma
update in ground static_2 basic_2 apps_2
[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / rt_transition / cpx_reqg.ma
index ae75c0089ef43125ea6b349d3e328eef40a5a86a..083b43e4758a526aa5fae78f56113471be27206e 100644 (file)
@@ -27,6 +27,6 @@ lemma cpx_reqg_conf_sn (S) (G):
 (* Basic_2A1: was just: cpx_lleq_conf_dx *)
 lemma cpx_reqg_conf_dx (S) (G) (L2):
       reflexive … S → symmetric … S →
-      â\88\80T1,T2. â\9dªG,L2â\9d« ⊢ T1 ⬈ T2 →
+      â\88\80T1,T2. â\9d¨G,L2â\9d© ⊢ T1 ⬈ T2 →
       ∀L1. L1 ≛[S,T1] L2 → L1 ≛[S,T2] L2.
 /4 width=4 by cpx_reqg_conf_sn, reqg_sym/ qed-.