-- Queries:
#check nat
ℕ : Type  #check bool
bool : Type

-- Proofs:
example (p q r : Prop) : p ∧ q ↔ q ∧ p :=
begin
p, q, r:Prop
p ∧ q ↔ q ∧ p
  apply iff.intro,
p, q, r:Prop
p ∧ q → q ∧ p
p, q, r:Prop
q ∧ p → p ∧ q
  intro H,
p, q, r:Prop
H:p ∧ q
q ∧ p
p, q, r:Prop
q ∧ p → p ∧ q
  apply and.intro,
p, q, r:Prop
H:p ∧ q
q
p, q, r:Prop
H:p ∧ q
p
p, q, r:Prop
q ∧ p → p ∧ q
  apply (and.elim_right H),
p, q, r:Prop
H:p ∧ q
p
p, q, r:Prop
q ∧ p → p ∧ q
  apply (and.elim_left H),
p, q, r:Prop
q ∧ p → p ∧ q
  intro H,
p, q, r:Prop
H:q ∧ p
p ∧ q
  apply and.intro,
p, q, r:Prop
H:q ∧ p
p
p, q, r:Prop
H:q ∧ p
q
  apply (and.elim_right H),
p, q, r:Prop
H:q ∧ p
q
  apply (and.elim_left H),
end