proposition: Lemma lhs_dp : incl (map lhs dp) (map lhs R).
proof: Proof. unfold incl. intros. ded (in_map_elim H). do 2 destruct H0. subst a. destruct x as [l r]. ded (dp_elim H0). do 2 destruct H1. change (In (lhs (mkRule l x)) (map lhs R)). apply in_map. exact H1. Qed.
imports: CoLoR(LogicUtil ATrs ACalls ACap ASN RelUtil ListUtil SN VecUtil VecOrd NatUtil BoolUtil)