proposition: Lemma try_coherent : coherent try_sp.
proof: Proof. case=>p H y m; split. - case=>i [x][h][/= H1][H2] H3. by exists i; exists H1; exists i; exists x; exists h. case=>i [/= H1][_][x][h][<-][T1 T2]. by exists i; exists x; exists h. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) LemmaOverloading(prelude heaps rels hprop domains)