Theory Peirce

subsection‹Peirce›

theory Peirce
  imports Types
begin
  
text‹As an example of our $\lambda\mu$ formalisation, we show show a
     $\lambda\mu$-term inhabiting Peirce's Law. The example is due to
     Parigot~\<^cite>‹"DBLP:conf/lpar/Parigot92"›.›  
    
text‹Peirce's law: $((A \rightarrow B) \rightarrow A) \rightarrow A$.›

lemma "Γ, Δ ⊢⇩T λ (A→B)→A: (μ A:(<0>((`0) ° (λ A: (μ B:(<1> (`0))))))) 
    : ((A→B)→A)→A"
  by fastforce    
    
end