Data Nat:* = O:Nat | S:(k:Nat)Nat;

plus : (m:Nat)(n:Nat)Nat;
intro m;
induction m;
intros;
fill n;
intros;
refine S;
fill k_IH n0; 
Qed;

adderType : (m:Nat)(n:Nat)*;
intros;
induction m;
fill Nat;
intros;
fill (n:Nat)k_IH;
Qed;

adder: (m:Nat)(n:Nat)(adderType m n);
intro m;
induction m;
intros;
fill n;
intros;
compute;
intros;
fill k_IH (plus n0 n1);
Qed;

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

fact:(m:Nat)Nat;
intros;
induction m;
fill (S O);
intros;
fill (mult (S k) k_IH);
Qed;


testval = fact (S (S (S (S (S (S (S (S (S O)))))))));

Data Vect (A:*):(n:Nat)* 
    = vnil:Vect A O
    | vcons:(k:Nat)(x:A)(xs:Vect A k)Vect A (S k);

vectsum : (k:Nat)(v:Vect Nat k)Nat;
intros;
induction v;
fill O;
intros;
fill (plus x xs_IH);
Qed;

testvect2 = vcons _ _ (S O) (vcons _ _ (S (S (S O))) (vnil Nat));
testval2 = vectsum _ testvect2;