Function unify 

pub fn unify(ctx: &Context, mctx: &mut MetaCtx, a: &Term, b: &Term) -> bool

First-order unification of a and b, solving metavariables into mctx. Returns whether they were made equal. A metavariable unifies with anything (after the occurs-check); everything else decomposes structurally.