module A201605.AltArtemov.Try3.Scratch where


{-


-------
⊥ type


A type    B type
----------------
(A ⊃ B) type


A type    B type
----------------
(A ∧ B) type


t term    A type
----------------
(t ∶ A) type




----------
Γ , A ⊢ A


-------------------------------
Γ , A ⊢ xₙ ∶ xₙ₋₁ ∶ … ∶ x ∶ A


Γ , A ⊢ B
----------
Γ ⊢ A ⊃ B


Γ , A ⊢ tₙ ∶ tₙ₋₁ ∶ … ∶ t ∶ B
-------------------------------------------
Γ ⊢ λⁿ tₙ ∶ λⁿ⁻¹ tₙ₋₁ ∶ … ∶ λ t ∶ (A ⊃ B)


Γ ⊢ A ⊃ B    Γ ⊢ A
--------------------
Γ ⊢ B


Γ ⊢ tₙ ∶ tₙ₋₁ ∶ … ∶ t ∶ (A ⊃ B)    Γ ⊢ sₙ ∶ sₙ₋₁ ∶ … ∶ s ∶ A
----------------------------------------------------------------
Γ ⊢ (tₙ ∘ⁿ sₙ) ∶ (tₙ₋₁ ∘ⁿ⁻¹ sₙ₋₁) ∶ … ∶ (t ∘ s) ∶ B


Γ ⊢ A    Γ ⊢ B
----------------
Γ ⊢ A ∧ B


Γ ⊢ tₙ ∶ tₙ₋₁ ∶ … ∶ t ∶ A    Γ ⊢ sₙ ∶ sₙ₋₁ ∶ … ∶ s ∶ B
--------------------------------------------------------------
Γ ⊢ pⁿ(tₙ , sₙ) ∶ pⁿ⁻¹(tₙ₋₁ , sₙ₋₁) ∶ … ∶ p(t , s) ∶ (A ∧ B)


Γ ⊢ A ∧ B
----------
Γ ⊢ A


Γ ⊢ tₙ ∶ tₙ₋₁ ∶ … ∶ t ∶ (A ∧ B)
----------------------------------------
Γ ⊢ π₀ⁿ tₙ ∶ π₀ⁿ⁻¹ tₙ₋₁ ∶ … ∶ π₀ t ∶ A


Γ ⊢ A ∧ B
----------
Γ ⊢ B


Γ ⊢ tₙ ∶ tₙ₋₁ ∶ … ∶ t ∶ (A ∧ B)
----------------------------------------
Γ ⊢ π₁ⁿ tₙ ∶ π₁ⁿ⁻¹ tₙ₋₁ ∶ … ∶ π₁ t ∶ B


𝒟 : Γ ⊢ A
------------
Γ ⊢ ⌊𝒟⌋ ∶ A


𝒟 : Γ ⊢ t ∶ A
----------------
Γ ⊢ ⌊𝒟⌋ ∶ t ∶ A


𝒟 : Γ ⊢ tₙ ∶ tₙ₋₁ ∶ … ∶ t ∶ A
---------------------------------
Γ ⊢ ⌊𝒟⌋ ∶ tₙ ∶ tₙ₋₁ ∶ … ∶ t ∶ A


Γ ⊢ ⌊𝒟⌋ ∶ A
------------
Γ ⊢ A


Γ ⊢ ⌊𝒟⌋ ∶ t ∶ A
----------------
Γ ⊢ t ∶ A


Γ ⊢ ⌊𝒟⌋ ∶ tₙ ∶ tₙ₋₁ ∶ … ∶ t ∶ A
---------------------------------
Γ ⊢ tₙ ∶ tₙ₋₁ ∶ … ∶ t ∶ A


-}