proposition: Lemma ProgOk_Chomp_lemma : forall `{FacadeWrapper (Value av) A} env key prog (tail1 tail2: A -> Telescope av) ext (v: A), key ∉ ext -> ({{ tail1 v }} prog {{ tail2 v }} ∪ {{ [key |> wrap v] :: ext }} // env <-> {{ Cons (NTSome key) (ret v) tail1 }} prog {{ Cons (NTSome key) (ret v) tail2 }} ∪ {{ ext }} // env).
proof: Proof. repeat match goal with | _ => progress intros | _ => progress split | _ => tauto | [ H: ?a /\ ?b |- _ ] => destruct H | [ H: ?a ≲ Cons _ _ _ ∪ _ |- _ ] => learn (Cons_PushExt _ _ _ _ _ H) | [ H: ProgOk ?fmap _ _ ?t1 ?t2, H': _ ≲ ?t1 ∪ ?fmap |- _ ] => destruct (H _ H'); no_duplicates | [ H: RunsTo _ _ ?from ?to, H': forall st, RunsTo _ _ ?from st -> _ |- _ ] => specialize (H' _ H) | [ H: _ ≲ _ ∪ [_ |> _] :: _ |- _ ] => apply Cons_PopExt in H | _ => solve [eauto using Cons_PopExt] end. Qed.
imports: Coq.Classes.Morphisms CertifiedExtraction.CoreLemmas CertifiedExtraction.PropertiesOfTelescopes CertifiedExtraction.PropertiesOfTelescopes CertifiedExtraction.FacadeLemmas