full.ma

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / grammar / bteq_bteq.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/bteq_bteq.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/bteq_bteq.ma
index 4dad596fd34531840b9d28b1869c84247d575abc..7870b26445e158215aac858d15c546407c5b5814 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/grammar/bteq_bteq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/bteq_bteq.ma
@@ -21,3 +21,11 @@ include "basic_2/grammar/bteq.ma".
 theorem bteq_trans: tri_transitive … bteq.
 #G1 #G #L1 #L #T1 #T * //
 qed-.
+
+theorem bteq_canc_sn: ∀G,G1,G2,L,L1,L2,T,T1,T2. ⦃G, L, T⦄ ⋕ ⦃G1, L1, T1⦄ →
+                      ⦃G, L, T⦄ ⋕ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ⋕ ⦃G2, L2, T2⦄.
+/3 width=5 by bteq_trans, bteq_sym/ qed-.
+
+theorem bteq_canc_dx: ∀G1,G2,G,L1,L2,L,T1,T2,T. ⦃G1, L1, T1⦄ ⋕ ⦃G, L, T⦄ →
+                      ⦃G2, L2, T2⦄ ⋕ ⦃G, L, T⦄ → ⦃G1, L1, T1⦄ ⋕ ⦃G2, L2, T2⦄.
+/3 width=5 by bteq_trans, bteq_sym/ qed-.