+
+lemma bi_TC_decomp_r: ∀A,B. ∀R:bi_relation A B.
+ ∀a1,a2,b1,b2. bi_TC … R a1 b1 a2 b2 →
+ R a1 b1 a2 b2 ∨
+ ∃∃a,b. bi_TC … R a1 b1 a b & R a b a2 b2.
+#A #B #R #a1 #a2 #b1 #b2 * -a2 -b2 /2 width=1/ /3 width=4/
+qed-.
+
+lemma bi_TC_decomp_l: ∀A,B. ∀R:bi_relation A B.
+ ∀a1,a2,b1,b2. bi_TC … R a1 b1 a2 b2 →
+ R a1 b1 a2 b2 ∨
+ ∃∃a,b. R a1 b1 a b & bi_TC … R a b a2 b2.
+#A #B #R #a1 #a2 #b1 #b2 #H @(bi_TC_ind_dx ?????????? H) -a1 -b1
+[ /2 width=1/
+| #a1 #a #b1 #b #Hab1 #Hab2 #_ /3 width=4/
+]
+qed-.