anchor.diff:      | Tm_uvar (u1, _), Tm_uvar (u2, _) ->
         equal_if (Unionfind.equiv u1 u2)
   
  -    | Tm_app (h1, args1), Tm_app(h2, args2) ->
  -      eq_and (eq_tm h1 h2) (fun () -> eq_args args1 args2)
  +    | Tm_app (h1, args1), Tm_app (h2, args2) ->
  +      begin match (un_uinst h1).n, (un_uinst h2).n with
  +      | Tm_fvar f1, Tm_fvar f2 when f1.fv_qual = Some Data_ctor && f2.fv_qual = Some Data_ctor ->
  +        // we got constructors! we know they are injective and disjoint, so we can do some
  +        // good analysis on them
  +        if fv_eq f1 f2
  +        then (
  +            assert (List.length args1 = List.length args2);
  +            List.fold_left (fun acc ((a1, q1), (a2, q2)) ->
  +                                assert (q1 = q2);
  +                                eq_inj acc (eq_tm a1 a2)) Equal <| List.zip args1 args2
  +        ) else NotEqual
  +      | _ -> // can only they're equal if they syntactically match, nothing else
  +          eq_and (eq_tm h1 h2) (fun () -> eq_args args1 args2)
  +      end
   
       | Tm_type u, Tm_type v ->
         equal_if (eq_univs u v)
  
positive.code:       | Equal -> g()
        | _ -> Unknown
      in
      match t1.n, t2.n with
      | Tm_name a, Tm_name b ->
        equal_if (bv_eq a b)
  
negative.code:     | Unknown
  
  let rec eq_tm (t1:term) (t2:term) : eq_result =
      let canon_app t =
          let hd, args = head_and_args' (unascribe t) in
          mk_Tm_app hd args None t.pos
      in
      let t1 = canon_app t1 in
      let t2 = canon_app t2 in
      let equal_if = function
          | true -> Equal
          | _ -> Unknown
  