Load "nat.tt";

code = {'(plus (S (S O)) (S (S O)))};

plusQ = [a:Nat][b:Nat]{'plus a b};

Check code;
Eval code;

Eval  !code;

test = [a:Nat]{'[b:Nat]~(plusQ a b)};

test2 = {'[A:*][x:{{A}}]~(!{'x})};



Eval test (S (S (S O)));
Eval !(test (S (S (S O)))) (S (S (S O)));

code2 = {'plus ~code ~code};
code3 = {'{'plus ~code ~code}};
code4 = [x:{{Nat}}]{'plus ~x ~x};

Eval code4 {'(plus (S O) (S O))};
Eval !(code4 {'(plus (S O) (S O))});

plusST : (m,n:{{Nat}}){{Nat}};
intros;
induction !m;
fill n;
intros;
fill {'S ~k_IH};
Qed;

val = code4 {'(plus (S O) (S O))};

Eval plusST val val;
Eval !(plusST val val);

Eval plusST;