Find file
Fetching contributors…
Cannot retrieve contributors at this time
17 lines (13 sloc) 224 Bytes
Load "lt.tt";
Data Fin : (n:Nat)* where
fz : (k:Nat)(Fin (S k))
| fs : (k:Nat)(i:Fin k)(Fin (S k));
mkFin : (m,n:Nat)(p:Lt m n)(Fin n);
intros;
induction p;
intros;
refine fz;
intros;
refine fs;
fill p_IH;
Qed;