ivor-0.1.5: examplett/lt.tt

Load "nat.tt";

Data Lt : (m,n:Nat)* where
    ltO : (m:Nat)Lt O (S m)
  | ltS : (m,n:Nat)(p:Lt m n)Lt (S m) (S n);

LtmSn : (m,n:Nat)(p:Lt m n)(Lt m (S n));
intros;
induction p;
intros;
refine ltO;
intros;
refine ltS;
fill p_IH;
Qed;

Ltmplus : (m,n,i:Nat)(p:Lt m n)(Lt m (plus n i));
intros;
induction p;
intros;
refine ltO;
intro m2 n1;
intros;
refine ltS;
fill p_IH;
Qed;