proposition: Lemma distribute_disj_imply: forall P Q R: Prop, ((P -> Q) /\ (R -> Q)) -> ((P \/ R) -> Q).
proof: Proof. intros. destruct H. destruct H0. apply H. trivial. apply H1. trivial. Qed.
imports: Coq(Bool Peano List PeanoNat) CoLoR(closure more_list equiv_list list_permut dickson) Coq(Relations Wellfounded Arith Wf_nat Recdef Program Morphisms Lia) CoLoR(term_spec term decidable_set ordered_set NatCompat)