proposition: Theorem O1_count_increases : forall d1 b1 c1 a2 b2 c2, In (d1, (b1, c1)) (getSupport (O1_count (b2, c2) a2)) -> c1 = S c2.
proof: Proof. intuition. unfold O1_count in *. fcf_simp_in_support. destruct x. fcf_simp_in_support. trivial. Qed.
imports: FCF.FCF FCF.RndInList