+
+lemma ibfr_beta_1 (v) (v1) (t) (q) (n):
+ q Ļµ šāØā»,nā© ā qāš±ān Ļµ t ā
+ ļ¼ v.ļ¼ v1.š.š.t ā”š¢šš[šāšāšāšāq] ļ¼ v.ļ¼ v1.š.š.(t[āqāš ”[š®āØāānā©]v]).
+#v #v1 #t #q #n #Hn #Ht
+@(ex6_5_intro ā¦ (š) (šāšāš) q (š) ā¦ Hn) -Hn
+[ //
+| /2 width=1 by pbc_empty, pbc_redex/
+| /3 width=1 by pcc_A_sn, pcc_L_sn, pcc_empty/
+| /5 width=1 by in_comp_appl_hd, in_comp_abst_hd/
+| @(subset_eq_canc_sn ā¦ (fsubst_appl_hd ā¦)) @appl_eq_repl [ // ]
+ @(subset_eq_canc_sn ā¦ (fsubst_appl_hd ā¦)) @appl_eq_repl [ // ]
+ @(subset_eq_canc_sn ā¦ (fsubst_abst_hd ā¦)) @abst_eq_repl
+ @(subset_eq_canc_sn ā¦ (fsubst_abst_hd ā¦)) @abst_eq_repl
+ @fsubst_eq_repl // <nplus_unit_sn @lift_term_eq_repl_dx
+ >list_cons_comm @(subset_eq_canc_sn ā¦ (grafted_appl_sd ā¦ ))
+ @(subset_eq_canc_sn ā¦ (grafted_empty_dx ā¦ )) //
+]
+qed.