test-polyrec.why 178 Bytes
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1

MARCHE Claude's avatar
MARCHE Claude committed
2

MARCHE Claude's avatar
MARCHE Claude committed
3 4
theory T

5
use option.Option
MARCHE Claude's avatar
MARCHE Claude committed
6 7 8 9 10 11 12 13 14

type t 'a = A | Lam (t (option 'a))

inductive r (t 'a) (t 'a) =
 | cas : forall x y:t (option 'a). r x y -> r (Lam x) (Lam y)

goal G : true

end