proposition: Lemma existsC_ind : forall (Q:Prop), (~~Q -> Q) -> (forall x:A, P x -> Q) -> existsC -> Q.
proof: Proof. intros Q HQ H ex. apply HQ. intros Z. apply ex. intros x Hx. apply Z. apply H with x. assumption. Qed.
imports: CoRN.stdlib_omissions.List