Specifications and proofs, independently checked

-- the language of propositional logic, and its rules
sort wff;
term im (p q: wff): wff;   infixr im: $->$ prec 25;
term not (p: wff): wff;    prefix not: $~$ prec 41;

axiom ax_1 (a b: wff): $ a -> b -> a $;
axiom ax_2 (a b c: wff): $ (a -> b -> c) -> (a -> b) -> a -> c $;
axiom ax_mp (a b: wff): $ a -> b $ > $ a $ > $ b $;

-- a claim, with no proof attached: this file only states it
theorem id (a: wff): $ a -> a $;

-- the same theorem, now proved -- the term after `=` is the proof
theorem a1i (h: $ b $): $ a -> b $ =
  '(ax_1 h);
theorem mpd (h1: $ a -> b $) (h2: $ a -> b -> c $): $ a -> c $ =
  '(ax_2 h2 h1);
theorem id: $ a -> a $ =
  '(mpd (! ax_1 _ a) ax_1);

-- Metamath C: a program whose type is a theorem about its output
(proc (adder {x : u32} {y : u32}
        : {ret : (sn {(cast {x + y}) : u64})})
  (sn {(cast {x + y}) : u64}))