(* Basic_2A1: includes: lreq_drop_trans_be *)
lemma seq_drops_trans_next: ∀f2,L1,L2. L1 ≡[f2] L2 →
- â\88\80b,f,I,K2. â\87©*[b,f] L2 â\89\98 K2.â\93\98[I] â\86\92 ð\9d\90\94â\9dªfâ\9d« →
+ â\88\80b,f,I,K2. â\87©*[b,f] L2 â\89\98 K2.â\93\98[I] â\86\92 ð\9d\90\94â\9d¨fâ\9d© →
∀f1. f ~⊚ ↑f1 ≘ f2 →
∃∃K1. ⇩*[b,f] L1 ≘ K1.ⓘ[I] & K1 ≡[f1] K2.
#f2 #L1 #L2 #HL12 #b #f #I2 #K2 #HLK2 #Hf #f1 #Hf2
(* Basic_2A1: includes: lreq_drop_conf_be *)
lemma seq_drops_conf_next: ∀f2,L1,L2. L1 ≡[f2] L2 →
- â\88\80b,f,I,K1. â\87©*[b,f] L1 â\89\98 K1.â\93\98[I] â\86\92 ð\9d\90\94â\9dªfâ\9d« →
+ â\88\80b,f,I,K1. â\87©*[b,f] L1 â\89\98 K1.â\93\98[I] â\86\92 ð\9d\90\94â\9d¨fâ\9d© →
∀f1. f ~⊚ ↑f1 ≘ f2 →
∃∃K2. ⇩*[b,f] L2 ≘ K2.ⓘ[I] & K1 ≡[f1] K2.
#f2 #L1 #L2 #HL12 #b #f #I1 #K1 #HLK1 #Hf #f1 #Hf2