proposition: Lemma miniChomp_arbitrary_post : forall `{FacadeWrapper (Value av) A} k (v: Comp A) tenv tenv' ext prog env, (forall vv, v ↝ vv -> {{ [[`k ->> vv as vv]] :: (tenv vv) }} prog {{ tenv' v }} ∪ {{ ext }} // env) -> {{ [[`k ~~> v as vv]] :: (tenv vv) }} prog {{ tenv' v }} ∪ {{ ext }} // env.
proof: Proof. miniChomp_t. Qed.
imports: Coq.Classes.Morphisms CertifiedExtraction.CoreLemmas CertifiedExtraction.PropertiesOfTelescopes CertifiedExtraction.PropertiesOfTelescopes CertifiedExtraction.FacadeLemmas