proposition: Lemma ProgOk_Transitivity_Name' : forall `{FacadeWrapper (Value av) A} k env ext t1 t2 prog1 prog2 (v: Comp A), {{ t1 }} prog1 {{ [[`k ~~> v as _]]::t1 }} ∪ {{ ext }} // env -> {{ [[`k ~~> v as _]]::t1 }} prog2 {{ [[v as kk]]::t2 kk }} ∪ {{ ext }} // env -> {{ t1 }} Seq prog1 prog2 {{ [[v as kk]]::t2 kk }} ∪ {{ ext }} // env.
proof: Proof. SameValues_Facade_t. Qed.
imports: CertifiedExtraction.StringMapUtils CertifiedExtraction.ExtendedLemmas CertifiedExtraction.TelAppend