+
+lemma l3_t12:
+ l3_t1 ➡𝐢𝐛𝐟[𝗟◗𝗔◗𝗔◗𝗟◗𝗟◗𝗔◗𝐞] l3_t2.
+@ibfr_abst_hd
+@ibfr_eq_trans
+[| @(ibfr_beta_1 … (𝟎)) [| <list_rcons_prop_1 ]
+ /2 width=3 by pcc_A_sn, in_comp_appl_hd/
+]
+@appl_eq_repl [ // ]
+@appl_eq_repl [ // ]
+@abst_eq_repl
+@abst_eq_repl
+@(subset_eq_canc_sn … (fsubst_appl_hd …))
+@appl_eq_repl [ // ]
+@(subset_eq_canc_sn … (fsubst_empty_rc …))
+@(subset_eq_canc_sn … (lift_term_oref_pap … )) //
+qed.