fact: Example chain4_prop : forall c₁ c₂ c₃ c₄ : Prop, forall e, (c₁ -> c₂ -> c₃ -> c₄) -> Id↓e ⊩ prop c₁ → prop c₂ → prop c₃ → prop c₄.
imports: Morphisms ClassicalRealizability.Tactics ClassicalRealizability.BasicResults ClassicalRealizability.Subtyping