module A201903.3-3-Properties-BigStep-CBV where
open import A201903.2-1-Semantics-BigStep
open CBV public
wnf-⟱ : ∀ {n} {e : Tm n} {e′} → e ⟱ e′ → WNF e′
wnf-⟱ (applam r₁ r₂ r) = wnf-⟱ r
wnf-⟱ var = wnf var
wnf-⟱ lam = lam
wnf-⟱ (app r₁ p₁′ r₂) = wnf (app p₁″ (wnf-⟱ r₂))
where
p₁″ = nawnf←wnf (wnf-⟱ r₁) p₁′
mutual
refl-⟱ : ∀ {n} {e : Tm n} → WNF e → e ⟱ e
refl-⟱ lam = lam
refl-⟱ (wnf p) = refl-⟱′ p
refl-⟱′ : ∀ {n} {e : Tm n} → NAWNF e → e ⟱ e
refl-⟱′ (var) = var
refl-⟱′ (app p₁ p₂) = app (refl-⟱′ p₁) (na←nawnf p₁) (refl-⟱ p₂)