{-# OPTIONS --guardedness --sized-types #-}
module A201903.3-6-Properties-BigStep-HS where
open import A201903.2-1-Semantics-BigStep
open HS public
hnf-⟱ : ∀ {n} {e : Tm n} {e′} → e ⟱ e′ → HNF e′
hnf-⟱ (applam r₁ r) = hnf-⟱ r
hnf-⟱ var = hnf var
hnf-⟱ (lam r) = lam (hnf-⟱ r)
hnf-⟱ (app r₁ p₁′) = hnf (app p₁″)
where
p₁″ = naxnf←hnf (hnf-⟱ r₁) p₁′
refl-⟱′ : ∀ {n} {e : Tm n} → NAXNF e → e ⟱ e
refl-⟱′ var = var
refl-⟱′ (app p₁) = app (refl-⟱′ p₁) (na←naxnf p₁)
refl-⟱ : ∀ {n} {e : Tm n} → HNF e → e ⟱ e
refl-⟱ (lam p) = lam (refl-⟱ p)
refl-⟱ (hnf p) = refl-⟱′ p