-- Live WebAssembly version of Lean
#eval let v := lean.version in let s := lean.special_version_desc in string.join
["Lean (version ", v.1.repr, ".", v.2.1.repr, ".", v.2.2.repr, ", ",
if s ≠ "" then s ++ ", " else s, "commit ", (lean.githash.to_list.take 12).as_string, ")"]

constants p q : Prop

def t1 : p → q → p := λ hp : p, λ hq : q, hp

/-- p → q → p is inhabited --/

theorem t2 : p → q → p := λ x : p, λ y : q, x 

theorem t3 : p → q → p :=
assume hp : p,
assume hq : q,
hp

theorem t4 : p → q → p :=
assume hp : p,
assume hq : q,
show p, from hp

theorem t5 (hp : p) (hq : q) : p := hp

/- The same as before -/

#check t1
#check t2
#check t5

/- axiom hp : p -/

theorem t6 : q → p := t1 hp

/- Universal statement -/

theorem t7 (p q : Prop) (hp : p) : p := sorry


theorem t8 : Π (p q : Prop), p → q → p := 
λ (p q : Prop) (hp : p) (hq : q), hp

#check t8

#check t8 (¬ p) (q)

variables p q : Prop

theorem t10 : p → q → p := λ (hp : p) (hq : q), hp

#check t10

variable hp : p

theorem t11 : q → p := λ (hq : q), hp

#check t11

/- Note that the type of t11 is the same as 
Π (p q : Prop) (hp : p) (hq : q), p -/

/- Π (p q : Prop), p → q → p -/

variables a b c e : Prop

#check t11 a b
#check t11 (b → c) (a → e)

variable h : b → c

#check t11 (b → c) (c → b) h

theorem t12 (h₁ : b → c) (h₂ : a → b) : a → c :=
assume h₃ : a,
show c, from h₁ (h₂ h₃)

#check t12