matita/matita/contribs/lambdadelta/basic_2/etc/tsts/tsts.etc

   1 fact tsts_inv_pair2_aux: ∀T1,T2. T1 ≂ T2 → ∀I,W2,U2. T2 = ②{I}W2.U2 →
   2                          ∃∃W1,U1. T1 = ②{I}W1.U1.
   3 #T1 #T2 * -T1 -T2
   4 [ #J #I #W2 #U2 #H destruct
   5 | #J #V1 #V2 #T1 #T2 #I #W2 #U2 #H destruct /2 width=3 by ex1_2_intro/
   6 ]
   7 qed-.
   8
   9 lemma tsts_inv_pair2: ∀I,T1,W2,U2. T1 ≂ ②{I}W2.U2 →
  10                       ∃∃W1,U1. T1 = ②{I}W1.U1.
  11 /2 width=5 by tsts_inv_pair2_aux/ qed-.