The Coq mailing list

[Victor Porton <porton AT narod.ru>]

Sorry, a modified version of this script. Why it yet does not work?

[[[[
Variable sub : Set->Set->Prop.

Variable A B C: Set.

Axiom ax1: (sub A B).
Axiom ax2: (sub B C).

Axiom sub_trans : forall a b c, sub a b -> sub b c -> sub a c.

Theorem thm: (sub A C).
proof.
  (*thus thesis by ax1, ax2, sub_trans using auto.*)
  thus thesis by ax1, ax2 using apply sub_trans.
end proof. Qed.
]]]]

18.11.2011, 21:17, "Victor Porton" 
<porton AT narod.ru>:
> Oh, see the version of my script without GAIA:
>
> [[[
> Variable sub : Set->Set->Prop.
>
> Variable A B C: Set.
>
> Axiom ax1: (sub A B).
> Axiom ax2: (sub B C).
>
> Theorem thm: (sub A C).
> proof.
> šš(*thus thesis by ax1, ax2, sub_trans using auto.*)
> ššthus thesis by ax1, ax2 using apply sub_trans.
> end proof. Qed.
> ]]]
>
> Why it does not verify and how to change it to make it working?
>
> --
> Victor Porton - http://portonvictor.org

-- 
Victor Porton - http://portonvictor.org