Theorem true_proof ≪ | index | src | ≫

\true证明

theorem true_proof: $ \true $;
StepHypRefExpression
1 imp_refl 
\fo x x = x \imp \fo x x = x
2 1 conv true 
\true

Axiom use

Logic (ax_mp, ax_1, ax_2)