]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/basic_2/etc/lsubr/lsubr_etc.etc
- extended multiple substitutions now uses bounds in ynat (ie. they
[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / etc / lsubr / lsubr_etc.etc
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 lemma lsubr_fwd_lsubr: ∀L1,L2. L1 ⓝ⊑ L2 → L1 ⊑ L2.
16 #L1 #L2 #H elim H -L1 -L2 // /2 width=1/
17 qed-.
18
19 lemma cpqs_cpr: ∀L,T1,T2. L ⊢ T1 ➤* T2 → L ⊢ T1 ➡ T2.
20 #L #T1 #T2 #H elim H -L -T1 -T2 // /2 width=1/ /2 width=6/
21 qed.
22
23 lemma cpss_cpr: ∀L,T1,T2. L ⊢ T1 ▶* T2 → L ⊢ T1 ➡ T2.
24 /3 width=1/ qed.
25
26 lemma lpqs_lpr: ∀L1,L2. L1 ⊢ ➤* L2 → L1 ⊢ ➡ L2.
27 #L1 #L2 #H elim H -L1 -L2 // /3 width=1/
28 qed.
29
30 lemma lpss_lpr: ∀L1,L2. L1 ⊢ ▶* L2 → L1 ⊢ ➡ L2.
31 /3 width=1/ qed.
32
33 lemma cpss_fwd_cir_eq: ∀L,T1,T2. L ⊢ T1 ▶* T2 → L ⊢ 𝐈⦃T1⦄ → T2 = T1.
34 /3 width=3 by cpr_fwd_cir, cpss_cpr/ qed-.
35
36 lemma cpss_cprs: ∀L,T1,T2. L ⊢ T1 ▶* T2 → L ⊢ T1 ➡* T2.
37 /3 width=1/ qed.
38
39 lemma cprs_cpss_trans: ∀L,T1,T. L ⊢ T1 ➡* T → ∀T2. L ⊢ T ▶* T2 → L ⊢ T1 ➡* T2.
40 /3 width=3/ qed-.
41
42 lemma cpss_cprs_trans: ∀L,T1,T. L ⊢ T1 ▶* T → ∀T2. L ⊢ T ➡* T2 → L ⊢ T1 ➡* T2.
43 /3 width=3/ qed-.
44
45 lemma cpcs_cpss_strap1: ∀L,T1,T. L ⊢ T1 ⬌* T → ∀T2. L ⊢ T ▶* T2 → L ⊢ T1 ⬌* T2.
46 #L #T1 #T #HT1 #T2 #HT2
47 @(cpcs_cpr_strap1 … HT1) -T1 /2 width=3/
48 qed-.
49
50 lemma cpcs_cpss_strap2: ∀L,T1,T. L ⊢ T1 ▶* T → ∀T2. L ⊢ T ⬌* T2 → L ⊢ T1 ⬌* T2.
51 #L #T1 #T #HT1 #T2 #HT2
52 @(cpcs_cpr_strap2 … HT2) -T2 /2 width=3/
53 qed-.
54
55 lemma cpcs_cpss_conf: ∀L,T,T1. L ⊢ T ▶* T1 → ∀T2. L ⊢ T ⬌* T2 → L ⊢ T1 ⬌* T2.
56 #L #T #T1 #HT1 #T2 #HT2
57 @(cpcs_cpr_conf … HT2) -T2 /2 width=3/
58 qed-.
59
60 lemma cpcs_cpss_div: ∀L,T1,T. L ⊢ T1 ⬌* T → ∀T2. L ⊢ T2 ▶* T → L ⊢ T1 ⬌* T2.
61 #L #T1 #T #HT1 #T2 #HT2
62 @(cpcs_cpr_div … HT1) -T1 /2 width=3/
63 qed-.
64