anchor.diff:     *   and then discharge it
      * 
      * Similarly for the g case
  +   *
  +   * 02/16/2021: We expect the `_` that we apply to subcomp to be instantiated
  +   *             by the unifier
  +   *
  +   *             However, in some cases, the binders that correspond to these `_`
  +   *             may be unconstrained, and hence we may fail in solving them
  +   *
  +   *             As an escape hatch, these binders can be decorated with
  +   *             the ite_soundness_forall attribute, in which case, instead of `_`,
  +   *             we use fresh names, essentially saying forall values of these
  +   *             binders, the proof should work
      *)
     let _if_then_else_is_sound = Errors.with_ctx "While checking if-then-else soundness" (fun () ->
       let r = (ed |> U.get_layered_if_then_else_combinator |> must |> snd).pos in
  
positive.code:           |> snd
            |> List.map (fun b -> b.binder_bv)
            |> List.map S.bv_to_name
            |> (fun l -> let (f::g::p::[]) = l in f, g, p) in
          Env.push_binders (Env.push_univ_vars env0 us) bs,
          S.mk_Tm_app ite_t
            (bs |> List.map (fun b -> S.bv_to_name b.binder_bv, binder_aq_to_arg_aq (b.binder_qual, b.binder_attrs)))
            r,
          f, g, p
        | _ -> failwith "Impossible! ite_t must have been an abstraction with at least 3 binders" in
  
      let subcomp_f, subcomp_g =
        let _, subcomp_t, subcomp_ty = stronger_repr in
        let _, subcomp_t = SS.open_univ_vars us subcomp_t in
  
        let aqs_except_last, last_aq =
          let _, subcomp_ty = SS.open_univ_vars us subcomp_ty in
          match (SS.compress subcomp_ty).n with
          | Tm_arrow (bs, _) ->
            let bs_except_last, last_b = bs |> List.splitAt (List.length bs - 1) in
            bs_except_last |> List.map (fun b -> b.binder_qual, b.binder_attrs),
            last_b |> List.hd |> (fun b -> b.binder_qual, b.binder_attrs)
          | _ -> failwith "Impossible! subcomp_ty must have been an arrow with at lease 1 binder" in
  
       let aqs_except_last, last_aq =
         aqs_except_last |> List.map binder_aq_to_arg_aq,
         last_aq |> binder_aq_to_arg_aq in
  
       let aux t =
        let tun_args = aqs_except_last |> List.map (fun aq -> S.tun, aq) in
  
        S.mk_Tm_app
          subcomp_t
          (tun_args@[t, last_aq])
          r in
  
       aux f_t, aux g_t in
  
      let tm_subcomp_ascribed_f, tm_subcomp_ascribed_g =
        let aux t =
  
negative.code:     let ite_us, ite_t, _ = if_then_else in
  
      let us, ite_t = SS.open_univ_vars ite_us ite_t in
      let env, ite_t_applied, a_b, f_t, g_t, p_t =
        match (SS.compress ite_t).n with
        | Tm_abs (bs, _, _) ->
          let bs = SS.open_binders bs in
  