test-polyrec.why 185 Bytes
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1 2 3 4 5 6 7 8 9 10 11 12 13

theory T

use import option.Option 

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