proposition: Lemma code_link_trim_right : ∀ A L E (v : raw_code A) p, ValidCode L E v → code_link v (trim E p) = code_link v p.
proof: Proof. intros A L E v p h. induction h in p |- *. - cbn. reflexivity. - cbn. rewrite lookup_op_trim. destruct lookup_op eqn:e. + cbn. rewrite H. f_equal. apply functional_extensionality. intuition auto. + cbn. eauto. - cbn. f_equal. apply functional_extensionality. intuition auto. - cbn. f_equal. intuition auto. - cbn. f_equal. apply functional_extensionality. intuition auto. Qed.
imports: Coq(Utf8) Relational(OrderEnrichedCategory OrderEnrichedRelativeMonadExamples) mathcomp(ssreflect eqtype choice seq ssrfun ssrbool ssrnat) extructures(ord fset fmap) Mon(SPropBase) Crypt(Prelude Axioms ChoiceAsOrd StateTransformingLaxMorph choice_type pkg_core_definition RulesStateProb) Equations(Equations)