matita/matita/contribs/lambdadelta/basic_2/etc/cpxs/cpxs.etc

   1 lemma lsubr_cpxs_trans: ∀h,o,G. lsub_trans … (cpxs h o G) lsubr.
   2 /3 width=5 by lsubr_cpx_trans, LTC_lsub_trans/
   3 qed-.
   4
   5 lemma cprs_cpxs: ∀h,o,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬈* T2 → ⦃G, L⦄ ⊢ T1 ⬈*[h] T2.
   6 #h #o #G #L #T1 #T2 #H @(cprs_ind … H) -T2 /3 width=3 by cpxs_strap1,
   7 cpr_cpx/
   8 qed.
   9
  10 lemma cpxs_inv_cnx1: ∀h,o,G,L,T,U. ⦃G, L⦄ ⊢ T ⬈*[h] U → ⦃G, L⦄ ⊢ ⬈[h] 𝐍⦃T⦄ → T = U.
  11 #h #o #G #L #T #U #H @(cpxs_ind_dx … H) -T //
  12 #T0 #T #H1T0 #_ #IHT #H2T0
  13 lapply (H2T0 … H1T0) -H1T0 #H destruct /2 width=1 by/
  14 qed-.
  15
  16 lemma cpxs_neq_inv_step_sn: ∀h,o,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → (T1 = T2 → ⊥) →
  17                             ∃∃T. ⦃G, L⦄ ⊢ T1 ⬈[h] T & T1 = T → ⊥ & ⦃G, L⦄ ⊢ T ⬈*[h] T2.
  18 #h #o #G #L #T1 #T2 #H @(cpxs_ind_dx … H) -T1
  19 [ #H elim H -H //
  20 | #T1 #T #H1 #H2 #IH2 #H12 elim (eq_term_dec T1 T) #H destruct
  21   [ -H1 -H2 /3 width=1 by/
  22   | -IH2 /3 width=4 by ex3_intro/ (**) (* auto fails without clear *)
  23   ]
  24 ]
  25 qed-.