Load "nat.tt";

-- plusST = lam m,n:{{Nat}}.
--    case !m of
--       O -> n
--       S k -> {'S ~(plusST ~k n)}

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

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

quote8 = plusST quote4 quote4;

Eval quote8;
Eval !quote8;

quotefoo = [m:Nat][n:Nat]{'plus (S (S O)) (([p:Nat](plus m p)) n)};

mult:(m,n:Nat)Nat;
intros;
induction m;
refine O;
intros;
refine (plus n k_IH);
Qed;

power:(m,x:Nat)Nat;
induction m;
fill (S O);
intros;
fill (mult x k_IH);
Qed;