q Ļµ šāØā»,nā© ā qāš±ān Ļµ t ā
ļ¼ v.š.t ā”š¢šš[šāšāq] ļ¼ v.š.(t[āqāš ”[š®āØānā©]v]).
#v #t #q #n #Hn #Ht
-@(ex6_5_intro ā¦ (š) (š) q (š) ā¦ Hn) -Hn //
-[ /3 width=1 by in_comp_appl_hd, in_comp_abst_hd/
+@(ex6_5_intro ā¦ (š) (š) q (š) ā¦ Hn) -Hn
+[ //
+| //
+| //
+| /3 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_abst_hd ā¦)) @abst_eq_repl
@fsubst_eq_repl // <nplus_zero_sn @lift_term_eq_repl_dx
@(subset_eq_canc_sn ā¦ (grafted_empty_dx ā¦ )) //
]
qed.
+
+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.