X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fdelayed_updating%2Freduction%2Fibfr_constructors.ma;h=112a98c3918eae4fd3d86fc64505d06cd575d790;hp=2a98609ad69ee662ded9f6c78296e4a88e6adc83;hb=cd2f5b59215ea771ac137b9a7b115a05175f45d5;hpb=513c4a61f11ce03888a8a0f9d8e513de6e3a7c8b

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr_constructors.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr_constructors.ma
index 2a98609ad..112a98c39 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr_constructors.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr_constructors.ma
@@ -68,8 +68,11 @@ lemma ibfr_beta_0 (v) (t) (q) (n):
       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
@@ -77,3 +80,22 @@ lemma ibfr_beta_0 (v) (t) (q) (n):
   @(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.