1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* IMMEDIATE BALANCED FOCUSED REDUCTION *************************************)
17 include "delayed_updating/reduction/ibfr.ma".
18 include "delayed_updating/substitution/fsubst_eq.ma".
19 include "delayed_updating/substitution/lift_prototerm_eq.ma".
21 (* Constructions with subset_equivalence ************************************)
23 lemma ibfr_eq_canc_sn (t) (t1) (t2) (r):
24 t ⇔ t1 → t ➡𝐢𝐛𝐟[r] t2 → t1 ➡𝐢𝐛𝐟[r] t2.
26 * #p #b #q #m #n #Hr#Hp #Hb #Hm #Hn #Ht #Ht2 destruct
27 @(ex7_5_intro … Hp Hb Hm Hn) [ // ] -Hp -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/
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/