higher-order prover のこと（３）

帰納法のユニファイもお任せです．

echo 'thf(nat,type,nat : $tType).
thf(z,type,z : nat).
thf(suc,type,suc : nat > nat).
thf(nat_induction,axiom,( ! [P : nat > $o] :
	(((P @ z) & (! [N : nat] : ((P @ N) => (P @ (suc @ N))))) =>
         (! [N : nat] : (P @ N))) )).
thf(x,type,x : $tType).
thf(f,type,f : nat > x).
thf(gl,conjecture,( (? [N : nat, M : nat] : (~ ( (f @ N) = (f @ M)))) 
=> (? [N : nat] : ( ( (f @ N) = (f @ z)) & ( ~ ((f @ (suc @ N)) = (f @ z))))) )).'> demo2.p
satallax -p coqscript -c ./demo2.v ./demo2.p
coqide ./demo2.v