+
+lemma lfxs_inv_lref_unit_sn: ∀R,L1,L2,i. L1 ⪤*[R, #i] L2 → ∀I,K1. ⬇*[i] L1 ≘ K1.ⓤ{I} →
+ ∃∃f,K2. ⬇*[i] L2 ≘ K2.ⓤ{I} & K1 ⪤*[cext2 R, cfull, f] K2 & 𝐈⦃f⦄.
+#R #L1 #L2 #i #HL12 #I #K1 #HLK1 elim (lfxs_dropable_sn … HLK1 … HL12 (#0)) -HLK1 -HL12 //
+#Y #HY #HLK2 elim (lfxs_inv_zero_unit_sn … HY) -HY
+#f #K2 #Hf #HK12 #H destruct /2 width=5 by ex3_2_intro/
+qed-.
+
+lemma lfxs_inv_lref_unit_dx: ∀R,L1,L2,i. L1 ⪤*[R, #i] L2 → ∀I,K2. ⬇*[i] L2 ≘ K2.ⓤ{I} →
+ ∃∃f,K1. ⬇*[i] L1 ≘ K1.ⓤ{I} & K1 ⪤*[cext2 R, cfull, f] K2 & 𝐈⦃f⦄.
+#R #L1 #L2 #i #HL12 #I #K2 #HLK2 elim (lfxs_dropable_dx … HL12 … HLK2 … (#0)) -HLK2 -HL12 //
+#Y #HLK1 #HY elim (lfxs_inv_zero_unit_dx … HY) -HY
+#f #K2 #Hf #HK12 #H destruct /2 width=5 by ex3_2_intro/
+qed-.