proposition: Lemma CompileSkip: forall {av} (ext : StringMap.t (Value av)) env tenv, {{ tenv }} Skip {{ tenv }} ∪ {{ ext }} // env.
proof: Proof. SameValues_Facade_t. Qed.
imports: CertifiedExtraction.StringMapUtils CertifiedExtraction.ExtendedLemmas CertifiedExtraction.TelAppend