Library sTactic
Theorem Contradict1 : forall a b : Prop, b -> (a -> ~ b) -> ~ a.
intuition.
Qed.
Theorem Contradict2 : forall a b : Prop, b -> ~ b -> a.
intuition.
Qed.
Theorem Contradict3 : forall a : Prop, a -> ~ ~ a.
auto.
Qed.
Ltac Contradict name :=
(apply (fun a : Prop => Contradict1 a _ name); clear name; intros name) ||
(apply (fun a : Prop => Contradict2 a _ name); clear name);
try apply Contradict3.
Ltac CaseEq name :=
generalize (refl_equal name); pattern name at -1 in |- *; case name.
Ltac Casec name := case name; clear name.
Ltac Elimc name := elim name; clear name.
Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (4 entries) |
Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (3 entries) |
Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (1 entry) |
Global Index
C
Contradict1 [lemma, in sTactic]Contradict2 [lemma, in sTactic]
Contradict3 [lemma, in sTactic]
S
sTactic [library]Lemma Index
C
Contradict1 [in sTactic]Contradict2 [in sTactic]
Contradict3 [in sTactic]
Library Index
S
sTacticGlobal Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (4 entries) |
Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (3 entries) |
Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (1 entry) |
This page has been generated by coqdoc