proposition: Lemma rule_partition_left : forall succ (succ_dec : rel_dec succ) l r rs, In (mkRule l r) (fst (partition (rule_partition succ_dec) rs)) -> partition_by_rel succ_dec (l, r) = true.
proof: Proof. intros. unfold rule_partition in H. set (w := partition_left (fun r => partition_by_rel succ_dec (lhs r, rhs r))). simpl in w. change l with (lhs (mkRule l r)). change r with (rhs (mkRule l r)). apply w with rs. hyp. Qed.
imports: CoLoR(ATrs RelUtil ListUtil ARelation SN LogicUtil)