proposition: Lemma interchange : ∀ A B C D E F L1 L2 L3 L4 p1 p2 p3 p4, ValidPackage L1 B A p1 → ValidPackage L2 E D p2 → ValidPackage L3 C B p3 → ValidPackage L4 F E p4 → trimmed A p1 → trimmed D p2 → Parable p3 p4 → par (link p1 p3) (link p2 p4) = link (par p1 p2) (par p3 p4).
proof: Proof. intros A B C D E F L1 L2 L3 L4 p1 p2 p3 p4 h1 h2 h3 h4 t1 t2 p34. apply eq_fmap. intro n. unfold par. rewrite unionmE. unfold link. rewrite !mapmE. rewrite unionmE. destruct (p1 n) as [[S1 [T1 f1]]|] eqn:e1. - simpl. f_equal. f_equal. f_equal. extensionality x. eapply trimmed_valid_Some_in in e1 as hi. 2,3: eauto. eapply from_valid_package in h1. specialize (h1 _ hi). cbn in h1. destruct h1 as [g [eg hg]]. rewrite e1 in eg. noconf eg. cbn in hg. erewrite code_link_par_left. 2: eapply hg. all: eauto. - simpl. destruct (p2 n) as [[S2 [T2 f2]]|] eqn:e2. + simpl. f_equal. f_equal. f_equal. extensionality x. eapply trimmed_valid_Some_in in e2 as hi. 2,3: eauto. eapply from_valid_package in h2. specialize (h2 _ hi). cbn in h2. destruct h2 as [g [eg hg]]. rewrite e2 in eg. noconf eg. cbn in hg. erewrite code_link_par_right. all: eauto. + simpl. reflexivity. 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)