]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_prototerm_eq.ma
24a3dbc602cb8c2062bf7bce37b812f0b3f62c0e
[helm.git] / matita / matita / contribs / lambdadelta / delayed_updating / substitution / lift_prototerm_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 include "ground/lib/subset_ext_equivalence.ma".
16 include "delayed_updating/substitution/lift_eq.ma".
17 include "delayed_updating/substitution/lift_prototerm.ma".
18
19 (* LIFT FOR PROTOTERM *******************************************************)
20
21 (* Constructions with subset_equivalence ************************************)
22
23 lemma lift_term_eq_repl_sn (f1) (f2) (t):
24       f1 ≗ f2 → ↑[f1]t ⇔ ↑[f2]t.
25 /3 width=1 by subset_equivalence_ext_f1_exteq, lift_path_eq_repl/
26 qed.
27
28 lemma lift_term_eq_repl_dx (f) (t1) (t2):
29       t1 ⇔ t2 → ↑[f]t1 ⇔ ↑[f]t2.
30 /2 width=1 by subset_equivalence_ext_f1_bi/
31 qed.
32
33 lemma lift_term_after (f1) (f2) (t):
34       ↑[f2]↑[f1]t ⇔ ↑[f2∘f1]t.
35 #f1 #f2 #t @subset_eq_trans
36 [
37 | @subset_inclusion_ext_f1_compose
38 | @subset_equivalence_ext_f1_exteq /2 width=5/
39 ]
40 qed.