13854.why 142 Bytes
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1
2
3
theory T
 type t 'a = A 'a | B

Andrei Paskevich's avatar
Andrei Paskevich committed
4
 function f () : ()
MARCHE Claude's avatar
MARCHE Claude committed
5
6
7
8
9
10
11

  goal g : () = f ()

  goal x : A () <> B
(*Theorem x : ((A ) = (B :(t unit))). *)

end