I have below statement in hypothesis
H: In S(S(S(S(S(S( a)))))) [2;3;4;5].
The natural number S(S(S(S(S(S( a)))))) will not exist in the list,for all vaues of a (0 or S a).
1) Could i prove above is wrong statement?
2) On the basis of this , H may i close any goal statement?
3) When simplify above, I get message " unknown a". How i can solve it?
1) Indeed the hypothesis
exfalso you can deduce any statement from a proof of
Here is some corresponding Coq code:
From Coq Require Import List. Import ListNotations. Goal forall P a, In (S(S(S(S(S(S(a))))))) [2;3;4;5] -> P. Proof. intros P a H. exfalso. repeat (destruct H; [ discriminate H | cbn in H ]). exact H. Qed.
Last updated: Oct 04 2023 at 22:01 UTC