proposition: Lemma code_link_id : ∀ A (v : raw_code A) L I, flat I → ValidCode L I v → code_link v (ID I) = v.
proof: Proof. intros A v L I h hv. induction hv. - cbn. reflexivity. - simpl. rewrite lookup_op_ID. 2: auto. rewrite H. simpl. f_equal. extensionality z. auto. - simpl. f_equal. apply functional_extensionality. auto. - simpl. f_equal. auto. - simpl. f_equal. apply functional_extensionality. 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)