24 lines
1.6 KiB
Text
24 lines
1.6 KiB
Text
det : ∀ {M M′ M″}
|
||
→ (M —→ M′)
|
||
→ (M —→ M″)
|
||
--------
|
||
→ M′ ≡ M″
|
||
det (ξ-·₁ L—→L′) (ξ-·₁ L—→L″) = cong₂ _·_ (det L—→L′ L—→L″) refl
|
||
det (ξ-·₁ L—→L′) (ξ-·₂ VL M—→M″) = ⊥-elim (V¬—→ VL L—→L′)
|
||
det (ξ-·₁ L—→L′) (β-ƛ _) = ⊥-elim (V¬—→ V-ƛ L—→L′)
|
||
det (ξ-·₂ VL _) (ξ-·₁ L—→L″) = ⊥-elim (V¬—→ VL L—→L″)
|
||
det (ξ-·₂ _ M—→M′) (ξ-·₂ _ M—→M″) = cong₂ _·_ refl (det M—→M′ M—→M″)
|
||
det (ξ-·₂ _ M—→M′) (β-ƛ VM) = ⊥-elim (V¬—→ VM M—→M′)
|
||
det (β-ƛ _) (ξ-·₁ L—→L″) = ⊥-elim (V¬—→ V-ƛ L—→L″)
|
||
det (β-ƛ VM) (ξ-·₂ _ M—→M″) = ⊥-elim (V¬—→ VM M—→M″)
|
||
det (β-ƛ _) (β-ƛ _) = refl
|
||
det (ξ-suc M—→M′) (ξ-suc M—→M″) = cong `suc_ (det M—→M′ M—→M″)
|
||
det (ξ-case L—→L′) (ξ-case L—→L″) = cong₄ case_[zero⇒_|suc_⇒_]
|
||
(det L—→L′ L—→L″) refl refl refl
|
||
det (ξ-case L—→L′) β-zero = ⊥-elim (V¬—→ V-zero L—→L′)
|
||
det (ξ-case L—→L′) (β-suc VL) = ⊥-elim (V¬—→ (V-suc VL) L—→L′)
|
||
det β-zero (ξ-case M—→M″) = ⊥-elim (V¬—→ V-zero M—→M″)
|
||
det β-zero β-zero = refl
|
||
det (β-suc VL) (ξ-case L—→L″) = ⊥-elim (V¬—→ (V-suc VL) L—→L″)
|
||
det (β-suc _) (β-suc _) = refl
|
||
det β-μ β-μ = refl
|