X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fsyntax%2Ftdeq_tdeq.ma;h=af82e7cd76d0ad7c7ae1986d6704a66318058d76;hb=e2b4ff64df523b4be9d7dc4e92386945846426e7;hp=9f47fd88f5fbeb8370b45f1f88bfef0b184c5f7d;hpb=1330e8b45155fc972bc18c4e5fd69897afa3cbe8;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/tdeq_tdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/tdeq_tdeq.ma
index 9f47fd88f..af82e7cd7 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/syntax/tdeq_tdeq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/tdeq_tdeq.ma
@@ -38,3 +38,13 @@ theorem tdeq_canc_dx: ∀h,o. right_cancellable … (tdeq h o).
 theorem tdeq_repl: ∀h,o,T1,T2. T1 ≡[h, o] T2 →
                    ∀U1. T1 ≡[h, o] U1 → ∀U2. T2 ≡[h, o] U2 → U1 ≡[h, o] U2.
 /3 width=3 by tdeq_canc_sn, tdeq_trans/ qed-.
+
+(* Negated main properies ***************************************************)
+
+theorem tdeq_tdneq_trans: ∀h,o,T1,T. T1 ≡[h, o] T → ∀T2. (T ≡[h, o] T2 → ⊥) →
+                          T1 ≡[h, o] T2 → ⊥.
+/3 width=3 by tdeq_canc_sn/ qed-.
+
+theorem tndeq_tdeq_canc_dx: ∀h,o,T1,T. (T1 ≡[h, o] T → ⊥) → ∀T2. T2 ≡[h, o] T →
+                            T1 ≡[h, o] T2 → ⊥.
+/3 width=3 by tdeq_trans/ qed-.