blob: 3e8bbeeb173fb261a40f2d23a4b29a8d6af15f69 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
|
(**** Tactics Tauto and Intuition ****)
(**** Tauto:
Tactic for automating proof in Intuionnistic Propositional Calculus, based on
the contraction-free LJT of Dickhoff ****)
(**** Intuition:
Simplifications of goals, based on LJT calcul ****)
(* Fails because Tauto does not perform any Apply *)
Goal ((A:Prop)A\/~A)->(x,y:nat)(x=y\/~x=y).
Proof.
Tauto.
|
