X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_transition%2Fcpx.ma;h=9900e8bf1cd088fcafad53a2a3633475df8fdc3d;hb=f6b452b9c9be141740d4058dfbcf81a4b75fd00b;hp=966e4a17eb25c3d3e8da3c12766de613bbed8d2e;hpb=88dd0e28758c693660a93ee0a9a5202c61ca09a0;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx.ma
index 966e4a17e..9900e8bf1 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx.ma
@@ -26,9 +26,6 @@ interpretation
 
 (* Basic properties *********************************************************)
 
-lemma cpx_atom: ∀h,I,G,L. ⦃G, L⦄ ⊢ ⓪{I} ⬈[h] ⓪{I}.
-/2 width=2 by cpg_atom, ex_intro/ qed.
-
 (* Basic_2A1: was: cpx_st *)
 lemma cpx_ess: ∀h,G,L,s. ⦃G, L⦄ ⊢ ⋆s ⬈[h] ⋆(next h s).
 /2 width=2 by cpg_ess, ex_intro/ qed.
@@ -91,6 +88,7 @@ lemma cpx_theta: ∀h,p,G,L,V1,V,V2,W1,W2,T1,T2.
 /3 width=4 by cpg_theta, ex_intro/
 qed.
 
+(* Basic_2A1: includes: cpx_atom *)
 lemma cpx_refl: ∀h,G,L. reflexive … (cpx h G L).
 /2 width=2 by ex_intro/ qed.