tests/test-and.why

   1
   2 theory And
   3
   4   type t1 =
   5     | A int real
   6     | B real int
   7     | C
   8
   9   type t2 =
  10     | D t1
  11     | E int
  12
  13   goal G : forall x:t2.
  14     match x with
  15     | D (((A i1 _) as t1) | ((B _ i1) as t1)) -> i1 = 2 /\ t1 <> C
  16     | D C -> x = E 1
  17     | E i -> i = 5 /\ i = 6
  18     end
  19
  20 end