changeset 5717 | 0d28dbe484b6 |
parent 5261 | ce3c25c8a694 |
child 9102 | c7ba07e3bbe8 |
5716:a3d2a6b6693e | 5717:0d28dbe484b6 |
---|---|
15 inductive IT |
15 inductive IT |
16 intrs |
16 intrs |
17 VarI "rs : lists IT ==> (Var n)$$rs : IT" |
17 VarI "rs : lists IT ==> (Var n)$$rs : IT" |
18 LambdaI "r : IT ==> Abs r : IT" |
18 LambdaI "r : IT ==> Abs r : IT" |
19 BetaI "[| (r[s/0])$$ss : IT; s : IT |] ==> (Abs r $ s)$$ss : IT" |
19 BetaI "[| (r[s/0])$$ss : IT; s : IT |] ==> (Abs r $ s)$$ss : IT" |
20 monos "[lists_mono]" |
20 monos lists_mono |
21 |
21 |
22 end |
22 end |