matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr_eq.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* IMMEDIATE BALANCED FOCUSED REDUCTION *************************************)
  16
  17 include "delayed_updating/reduction/ibfr.ma".
  18 include "delayed_updating/substitution/fsubst_eq.ma".
  19 include "delayed_updating/substitution/lift_prototerm_eq.ma".
  20
  21 (* Constructions with subset_equivalence ************************************)
  22
  23 lemma ibfr_eq_canc_sn (t) (t1) (t2) (r):
  24       t ⇔ t1 → t ➡𝐢𝐛𝐟[r] t2 → t1 ➡𝐢𝐛𝐟[r] t2.
  25 #t #t1 #t2 #r #Ht1
  26 * #p #b #q #m #n #Hr #Hb #Hm #Hn #Ht #Ht2 destruct
  27 @(ex6_5_intro … p … Hb Hm Hn) [ // ] -Hb -Hm -Hn
  28 [ /2 width=3 by subset_in_eq_repl_back/
  29 | /5 width=3 by subset_eq_canc_sn, fsubst_eq_repl, lift_term_eq_repl_dx, grafted_eq_repl/
  30 ]
  31 qed-.
  32
  33 lemma ibfr_eq_repl (t1) (t2) (u1) (u2) (r):
  34       t1 ⇔ u1 → t2 ⇔ u2 → t1 ➡𝐢𝐛𝐟[r] t2 → u1 ➡𝐢𝐛𝐟[r] u2.
  35 /3 width=3 by ibfr_eq_canc_sn, ibfr_eq_trans/
  36 qed-.