-
-lemma fqup_fpbg: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >[h, g] ⦃G2, L2, T2⦄.
-#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … L2 T2 H) -G2 -L2 -T2
-/4 width=5 by fpbg_strap1, fpbc_fpbg, fpbc_fqu, fpb_fquq, fqu_fquq/
-qed.
-
-lemma cpxs_fpbg: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2 → (T1 = T2 → ⊥) →
- ⦃G, L, T1⦄ >[h, g] ⦃G, L, T2⦄.
-#h #g #G #L #T1 #T2 #H @(cpxs_ind … H) -T2
-[ #H elim H //
-| #T #T2 #_ #HT2 #IHT1 #HT12
- elim (term_eq_dec T1 T) #H destruct
- [ -IHT1 /4 width=1/
- | lapply (IHT1 … H) -IHT1 -H -HT12 #HT1
- @(fpbg_strap1 … HT1) -HT1 /2 width=1 by fpb_cpx/
- ]
-]
-qed.
-
-lemma cprs_fpbg: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡* T2 → (T1 = T2 → ⊥) →
- ⦃G, L, T1⦄ >[h, g] ⦃G, L, T2⦄.
-/3 width=1 by cprs_cpxs, cpxs_fpbg/ qed.