+(*
+lemma tpr_conf_aux:
+ ∀T. (
+ ∀T1. #T1 < #T → ∀T3,T4. T1 ⇒ T3 → T1 ⇒ T4 →
+ ∃∃T0. T3 ⇒ T0 & T4 ⇒ T0
+ ) →
+ ∀U1,T1,T2. U1 ⇒ T1 → U1 ⇒ T2 → U1 = T →
+ ∃∃T0. T1 ⇒ T0 & T2 ⇒ T0.
+#T #IH #U1 #T1 #T2 * -U1 T1
+[ #k1 #H1 #H2 destruct -T;
+ lapply (tpr_inv_sort1 … H1) -H1
+(* case 1: sort, sort *)
+ #H1 destruct -T2 //
+| #i1 #H1 #H2 destruct -T;
+ lapply (tpr_inv_lref1 … H1) -H1
+(* case 2: lref, lref *)
+ #H1 destruct -T2 //
+| #I1 #V11 #V12 #T11 #T12 #HV112 #HT112 #H1 #H2 destruct -T;
+ lapply (tpr_inv_bind1 … H1) -H1
+ [