prove complete preservation

[ivoysey]

  complete-preservation : {Δ : hctx} {e : hexp} {d d' : dhexp} {τ : htyp} →
             ecomplete e →
             ∅ ⊢ e ⇒ τ ~> d ⊣ Δ →
             Δ ⊢ d ↦ d' →
             Δ , ∅ ⊢ d' :: τ

@cyrus- said one or both of these was trivial and should be removed but i forget which one

[cyrus-]

I think this one is trivial? No need to remove it though, just prove it.

…

On Thu, Dec 7, 2017 at 7:01 PM Ian Voysey ***@***.***> wrote: complete-preservation : {Δ : hctx} {e : hexp} {d d' : dhexp} {τ : htyp} → ecomplete e → ∅ ⊢ e ⇒ τ ~> d ⊣ Δ → Δ ⊢ d ↦ d' → Δ , ∅ ⊢ d' :: τ @cyrus- <https://github.com/cyrus-> said one or both of these was trivial and should be removed but i forget which one — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#7>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AARIPvo4gHX62rd8P-NMsMNmPtpXvNoGks5s-IpbgaJpZM4Q6beE> .

[ivoysey]

OK, yeah. I'll add full preservation as a postulate until I finish it so that I can confirm it's as we think. (Agda doesn't let you import modules that have holes in them, which is probably a good idea, and I already have the muscle memory of grep postulate before considering something to be finished.)