matita/matita/contribs/lambdadelta/basic_2/etc/fleq/fpbs.etc

   1 (* alternative proof that needs decidability of bteq to go in fpbs.ma
   2  * or lpx_fpbc_trans to go in fpbs_lift.ma (possibly)
   3 *)
   4
   5 axiom lpx_bteq_trans: ∀h,g,G1,G2,L1,L,L2,T1,T2. ⦃G1, L1⦄ ⊢➡ [h, g] L →
   6                       ⦃G1, L, T1⦄ ⋕[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ⋕[h, g] ⦃G2, L2, T2⦄.
   7
   8 lemma fpbs_fwd_fpb_sn: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄ →
   9                        ⦃G1, L1, T1⦄ ⋕[h, g] ⦃G2, L2, T2⦄ ∨
  10                        ∃∃G,L,T. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G, L, T⦄ & ⦃G, L, T⦄ ≥[h, g] ⦃G2, L2, T2⦄.
  11 #h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fpbs_ind_dx … H) -G1 -L1 -T1 [ /2 width=1 by or_introl/ ] (**) (* auto fails without brackets *)
  12 #G1 #G #L1 #L #T1 #T *
  13 [ #G0 #L0 #T0 #H #H02 #IH1 elim (fquq_inv_gen … H) -H
  14   [ -IH1 /4 width=5 by fpbc_fqu, ex2_3_intro, or_intror/
  15   | -H02 * #HG #HL #HT destruct /2 width=1 by/
  16   ]
  17 | #T0 #HT10 #H02 #IH02 elim (eq_term_dec T1 T0) #H destruct
  18   [ -H02 /2 width=1 by/
  19   | -IH02 /5 width=5 by fpbc_cpx, ex2_3_intro, or_intror/
  20   ]
  21 | #L0 #HL10 #_ * [ /3 width=3 by or_introl, lpx_bteq_trans/ ]
  22   * #G3 #L3 #T3 #H13 #H32