fact: Structure ast (i j : ctx) (t : synheap) := Ast {heap_of :> tagged_heap; _ : invariant i j t heap_of}.
imports: mathcomp(ssreflect ssrfun ssrbool ssrnat seq eqtype) LemmaOverloading(prelude prefix xfind heaps terms)