(define pf prove-from)

(define id-axiom (forall ?x (= ?x ?x)))


(structure (BTree S)
  (leaf S)
  (root (BTree S) (BTree S)))



(declare mirror ((S) -> ((BTree S)) (BTree S)))


(define mirror-axiom-1
  (forall ?x
    (= (mirror (leaf ?x)) (leaf ?x))))


(define mirror-axiom-2
  (forall ?t1 ?t2
    (= (mirror (root ?t1 ?t2))
       (root (mirror ?t2) (mirror ?t1)))))

(assert mirror-axiom-1 mirror-axiom-2)

(define (goal t)
  (= (mirror (mirror t)) t))

(by-induction-on ?t (goal ?t)
  ((leaf x) (!pf (goal (leaf x)) [mirror-axiom-1]))
  ((root t1 t2) (!pf (goal (root t1 t2)) [(goal t1) (goal t2) mirror-axiom-2 id-axiom])))