proposition: Lemma mkdp_app : forall l1 l2, mkdp (l1 ++ l2) = mkdp l1 ++ mkdp l2.
proof: Proof. induction l1; simpl; intros. refl. destruct a as [l r]. rewrite app_ass, IHl1. refl. Qed.
imports: CoLoR(LogicUtil ATrs ACalls ACap ASN RelUtil ListUtil SN VecUtil VecOrd NatUtil BoolUtil)