proposition: Lemma code_link_scheme : ∀ L A c p, @ValidCode L [interface] A c → code_link c p = c.
proof: Proof. intros L A c p h. induction h. - reflexivity. - eapply fromEmpty. rewrite fset0E. eauto. - simpl. f_equal. apply functional_extensionality. intro. eauto. - simpl. f_equal. eauto. - simpl. f_equal. apply functional_extensionality. intro. eauto. Qed.
imports: mathcomp(all_ssreflect all_algebra reals distr fingroup.fingroup realsum ssrnat ssreflect ssrfun ssrbool ssrnum eqtype choice seq) extructures(ord fset fmap) Crypt(Axioms Prelude pkg_core_definition pkg_composition pkg_notation RulesStateProb pkg_advantage pkg_lookup pkg_semantics pkg_heap pkg_invariants pkg_distr pkg_rhl pkg_tactics choice_type) Coq(Utf8 FunctionalExtensionality Setoids.Setoid Classes.Morphisms) Equations(Equations)