theory lcbdef imports lcrdef begin inductive "redstd sn ty" intros (* argI: M --> M N *) argI : "(N, a) : wty Int sn ==> (M, a -> b) : wty ==> (a -> b) = ty ==> (App M N, M) : redstd sn ty" consts wtrib :: "lct relation" ltlt :: "lct relation" sn1a :: "lct relation => lct relation" inductive "wtrib" intros (* types unspecified in the following *) isI : "(b, App a b) : wtrib" xI : "(b, e) : wtrib ==> (b, App e a) : wtrib" fI : "(M', M) : wtri ==> (Lam aty M', Lam aty M) : wtrib" inductive "sn1a r" intros I : "(t, s) : fctxt (inarg (fwf (ctxt r))) ==> (t, s) : sn1a r" inductive "ltlt" intros tylessI : "(t, tyt) : wty ==> (s, tys) : wty ==> (tyt, tys) : pSubty ==> (t, s) : ltlt" sn1I : "(t, s) : sn1a (beta Un eta) ==> (t, s) : ltlt" end