•Cons
:: (n=(S m)) =>a -> (Seq a m) -> (Seq a n)
•When applying a
constructor, the equality must be satisfied
from a set of known facts
–Given x : a,
– y : Seq a m
– Cons x y :: Seq a n
–Provided we can prove the
obligation: n=S m
•New known facts are
introduced when pattern matching against
a qualified constructor
–The defintion: f ((Cons x y)::Seq a n) = . . .
–x::a, y::Seq a m and the fact that n=S m
•Equalities in
obligations are solved using the facts by a decision procedure