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

   1 (*
   2 lemma lprs_fpbs: ∀h,o,G,L1,L2,T. ⦃G, L1⦄ ⊢ ➡* L2 → ⦃G, L1, T⦄ ≥[h, o] ⦃G, L2, T⦄.
   3 /3 width=1 by lprs_lpxs, lpxs_fpbs/ qed.
   4
   5 (* Note: this is used in the closure proof *)
   6 lemma cpr_lpr_fpbs: ∀h,o,G,L1,L2,T1,T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ⦃G, L1⦄ ⊢ ➡ L2 →
   7                     ⦃G, L1, T1⦄ ≥[h, o] ⦃G, L2, T2⦄.
   8 /4 width=5 by fpbs_strap1, fpbq_fpbs, lpr_fpbq, cpr_fpbq/
   9 qed.
  10 *)