-- Queries:-- Proofs: example (p q r : Prop) : p ∧ q ↔ q ∧ p :=p, q, r:Propp ∧ q ↔ q ∧ pp, q, r:Propp ∧ q → q ∧ pp, q, r:Propq ∧ p → p ∧ qp, q, r:PropH:p ∧ qq ∧ pp, q, r:Propq ∧ p → p ∧ qp, q, r:PropH:p ∧ qqp, q, r:PropH:p ∧ qpp, q, r:Propq ∧ p → p ∧ qp, q, r:PropH:p ∧ qpp, q, r:Propq ∧ p → p ∧ qp, q, r:Propq ∧ p → p ∧ qp, q, r:PropH:q ∧ pp ∧ qp, q, r:PropH:q ∧ ppp, q, r:PropH:q ∧ pqapply (and.elim_left H), endp, q, r:PropH:q ∧ pq