mirror of
https://github.com/AdaCore/alt-ergo.git
synced 2026-02-12 12:39:26 -08:00
12 lines
183 B
Plaintext
12 lines
183 B
Plaintext
|
|
type t = A | B | C | D
|
|
type t2 = E | F | G | H
|
|
|
|
goal g2 :
|
|
forall a : (t,t2) farray.
|
|
a[B <- E][A] <> E ->
|
|
a[C <- F][A] <> F ->
|
|
a[D <- G][A] <> G ->
|
|
a[A] = H
|
|
|