proposition: Lemma CompileSeq : forall {av} (tenv1 tenv1' tenv2: Telescope av) ext env p1 p2, {{ tenv1 }} p1 {{ tenv1' }} ∪ {{ ext }} // env -> {{ tenv1' }} p2 {{ tenv2 }} ∪ {{ ext }} // env -> {{ tenv1 }} (Seq p1 p2) {{ tenv2 }} ∪ {{ ext }} // env.
proof: Proof. SameValues_Facade_t. Qed.
imports: CertifiedExtraction.StringMapUtils CertifiedExtraction.ExtendedLemmas CertifiedExtraction.TelAppend