proposition: Lemma impdec : forall P Q : Prop, P \/ ~ P -> Q \/ ~ Q -> (P -> Q) \/ ~ (P -> Q).
proof: Proof. intros. elim H. elim H0. left. intros. assumption. right. intro. apply H1. apply H3. assumption. left. intros. elim H1. assumption. Qed.
imports: Arith ZArith EqNat