define (sub-helper1 [] ?t ?f) (?t)

define (sub-helper1 (?p :: ?ps) ?t ?f) (if (?p) (then (sub-helper1 ?ps ?t ?f)) (else ?f))

define (sub-helper ?x1 ?x2) (if (isVar ?x1) (then ?x2) (else ?x1))

define (sub (?x1 (?y1 ?z1)) (?x2 (?y2 ?z2)) (?x3 (?y3 ?z3))) (sub-helper1 ((?x1 == ?x3) :: ((?y1 == ?y3) :: ((?z1 == ?z3) :: []))) ((sub-helper ?x2 ?x3) ((sub-helper ?y2 ?y3) (sub-helper ?z2 ?z3))) (?x3 (?y3 ?z3)))