proposition: Lemma code_link_par_left : ∀ A I L L' E (v : raw_code A) p1 p2, ValidCode L E v → ValidPackage L' I E p1 → code_link v (par p1 p2) = code_link v p1.
proof: Proof. intros A I L L' E v p1 p2 hv hp1. unfold ValidCode in hv. induction hv. - cbn. reflexivity. - simpl. rewrite lookup_op_unionm. eapply lookup_op_valid in hp1 as hf. 2: eauto. destruct hf as [f [e hf]]. rewrite e. eapply lookup_op_spec in e as e'. rewrite e'. cbn. f_equal. extensionality z. eauto. - simpl. f_equal. extensionality x. eauto. - simpl. f_equal. eauto. - simpl. f_equal. extensionality x. eauto. 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)