matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_fqus.ma

   1 lemma csx_fqu_conf: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ →
   2                     ⦃G1, L1⦄ ⊢ ⬈*[h, o] T1 → ⦃G2, L2⦄ ⊢ ⬈*[h, o] T2.
   3 #h #o #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
   4 /2 width=8 by csx_inv_lref_bind, csx_inv_lift, csx_fwd_flat_dx, csx_fwd_bind_dx, csx_fwd_pair_sn/
   5 qed-.
   6
   7 lemma csx_fquq_conf: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮ ⦃G2, L2, T2⦄ →
   8                      ⦃G1, L1⦄ ⊢ ⬈*[h, o] T1 → ⦃G2, L2⦄ ⊢ ⬈*[h, o] T2.
   9 #h #o #G1 #G2 #L1 #L2 #T1 #T2 #H12 #H elim (fquq_inv_gen … H12) -H12
  10 [ /2 width=5 by csx_fqu_conf/
  11 | * #HG #HL #HT destruct //
  12 ]
  13 qed-.
  14
  15 lemma csx_fqup_conf: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐+ ⦃G2, L2, T2⦄ →
  16                      ⦃G1, L1⦄ ⊢ ⬈*[h, o] T1 → ⦃G2, L2⦄ ⊢ ⬈*[h, o] T2.
  17 #h #o #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2
  18 /3 width=5 by csx_fqu_conf/
  19 qed-.
  20
  21 lemma csx_fqus_conf: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐* ⦃G2, L2, T2⦄ →
  22                      ⦃G1, L1⦄ ⊢ ⬈*[h, o] T1 → ⦃G2, L2⦄ ⊢ ⬈*[h, o] T2.
  23 #h #o #G1 #G2 #L1 #L2 #T1 #T2 #H12 #H elim (fqus_inv_gen … H12) -H12
  24 [ /2 width=5 by csx_fqup_conf/
  25 | * #HG #HL #HT destruct //
  26 ]
  27 qed-.
  28