.. package:gdp

Given a value and a proof, attach the proof as a ghost proof on the value.

Apply an implication to the ghost proof attached to a value, leaving the value unchanged.

Take a simple function with one named argument and a named return, plus an implication relating a precondition to a postcondition of the function, and produce a function between refined input and output types.

newtype NonEmpty xs = NonEmpty Defn
type role Nonempty nominal -- disallows coercion of Nonempty's argument.

newtype Reverse  xs = Reverse  Defn
type role Reverse nominal

rev :: ([a] ~~ xs) -> ([a] ~~ Reverse xs)
rev xs = defn (reverse (the xs))

rev_nonempty_lemma :: NonEmpty xs -> Proof (NonEmpty (Reverse xs))

rev' :: ([a] ?NonEmpty) -> ([a] ?NonEmpty)
rev' = rev ...? rev_nonempty_lemma