matita/matita/contribs/lambdadelta/basic_2A/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