Z3---4.15.1.THM-Prf.s

%------------------------------------------------------------------------------
% File     : Z3---4.15.1
% Problem  : SCT155+1 : TPTP v9.0.0. Released v5.2.0.
% Transfm  : none
% Format   : tptp
% Command  : run_E %s %d THM

% Computer : n009.cluster.edu
% Model    : x86_64 x86_64
% CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory   : 8042.1875MB
% OS       : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit  : 300s
% DateTime : Sat Jun 21 05:24:33 AM UTC 2025

% Result   : Theorem 0.41s 0.58s
% Output   : Proof 0.48s
% Verified : 
% SZS Type : Refutation
%            Derivation depth      :    8
%            Number of leaves      :   26
% Syntax   : Number of formulae    :   58 (  17 unt;   0 typ;   0 def)
%            Number of atoms       :  820 ( 254 equ)
%            Maximal formula atoms :   40 (  14 avg)
%            Number of connectives :  983 ( 267   ~; 400   |;   1   &)
%                                         ( 234 <=>;  81  =>;   0  <=;   0 <~>)
%            Maximal formula depth :   19 (   7 avg)
%            Maximal term depth    :    4 (   1 avg)
%            Number of FOOLs       :   46 (  46 fml;   0 var)
%            Number of types       :    2 (   0 usr)
%            Number of type conns  :    0 (   0   >;   0   *;   0   +;   0  <<)
%            Number of predicates  :    7 (   5 usr;   1 prp; 0-3 aty)
%            Number of functors    :   16 (  16 usr;  11 con; 0-6 aty)
%            Number of variables   :  205 ( 186   !;   0   ?; 205   :)

% Comments : 
%------------------------------------------------------------------------------
tff(c_member_type,type,
    c_member: ( $i * $i * $i ) > $o ).

tff(hAPP_type,type,
    hAPP: ( $i * $i ) > $i ).

tff(tptp_fun_B_i_1_type,type,
    tptp_fun_B_i_1: ( $i * $i * $i * $i * $i * $i ) > $i ).

tff(v_P_H_____type,type,
    v_P_H____: $i ).

tff(v_P_____type,type,
    v_P____: $i ).

tff(v_b_H_____type,type,
    v_b_H____: $i ).

tff(v_a_H_____type,type,
    v_a_H____: $i ).

tff(v_b_____type,type,
    v_b____: $i ).

tff(v_a_____type,type,
    v_a____: $i ).

tff(c_Product__Type_OPair_type,type,
    c_Product__Type_OPair: ( $i * $i * $i * $i ) > $i ).

tff(tc_Arrow__Order__Mirabelle_Oalt_type,type,
    tc_Arrow__Order__Mirabelle_Oalt: $i ).

tff(tc_prod_type,type,
    tc_prod: ( $i * $i ) > $i ).

tff(v_F_type,type,
    v_F: $i ).

tff(c_Arrow__Order__Mirabelle_OProf_type,type,
    c_Arrow__Order__Mirabelle_OProf: $i ).

tff(tc_fun_type,type,
    tc_fun: ( $i * $i ) > $i ).

tff(tc_HOL_Obool_type,type,
    tc_HOL_Obool: $i ).

tff(tc_Arrow__Order__Mirabelle_Oindi_type,type,
    tc_Arrow__Order__Mirabelle_Oindi: $i ).

tff(1,plain,
    ( ~ ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a____,v_b____),hAPP(v_F,v_P____))
      <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(v_F,v_P_H____)) )
  <=> ~ ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a____,v_b____),hAPP(v_F,v_P____))
      <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(v_F,v_P_H____)) ) ),
    inference(rewrite,[status(thm)],[]) ).

tff(2,axiom,
    ~ ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a____,v_b____),hAPP(v_F,v_P____))
    <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(v_F,v_P_H____)) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_0) ).

tff(3,plain,
    ~ ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a____,v_b____),hAPP(v_F,v_P____))
    <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(v_F,v_P_H____)) ),
    inference(modus_ponens,[status(thm)],[2,1]) ).

tff(4,plain,
    ~ ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a____,v_b____),hAPP(v_F,v_P____))
    <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(v_F,v_P_H____)) ),
    inference(modus_ponens,[status(thm)],[3,1]) ).

tff(5,plain,
    ~ ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a____,v_b____),hAPP(v_F,v_P____))
    <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(v_F,v_P_H____)) ),
    inference(modus_ponens,[status(thm)],[4,1]) ).

tff(6,plain,
    ~ ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a____,v_b____),hAPP(v_F,v_P____))
    <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(v_F,v_P_H____)) ),
    inference(modus_ponens,[status(thm)],[5,1]) ).

tff(7,plain,
    ~ ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a____,v_b____),hAPP(v_F,v_P____))
    <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(v_F,v_P_H____)) ),
    inference(modus_ponens,[status(thm)],[6,1]) ).

tff(8,plain,
    ^ [V_P_Ha_2: $i,V_Pa_2: $i,V_b_Ha_2: $i,V_a_Ha_2: $i,V_ba_2: $i,V_aa_2: $i] :
      refl(( ( ( V_aa_2 = V_ba_2 )
          | ( V_aa_2 = V_b_Ha_2 )
          | ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(v_F,V_Pa_2))
          <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(v_F,V_P_Ha_2)) )
          | ( V_ba_2 = V_a_Ha_2 )
          | ( V_a_Ha_2 = V_b_Ha_2 )
          | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_P_Ha_2,c_Arrow__Order__Mirabelle_OProf)
          | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_Pa_2,c_Arrow__Order__Mirabelle_OProf)
          | ~ ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(V_Pa_2,tptp_fun_B_i_1(V_aa_2,V_ba_2,V_a_Ha_2,V_b_Ha_2,V_Pa_2,V_P_Ha_2)))
            <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(V_P_Ha_2,tptp_fun_B_i_1(V_aa_2,V_ba_2,V_a_Ha_2,V_b_Ha_2,V_Pa_2,V_P_Ha_2))) ) )
      <=> ( ( V_aa_2 = V_ba_2 )
          | ( V_aa_2 = V_b_Ha_2 )
          | ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(v_F,V_Pa_2))
          <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(v_F,V_P_Ha_2)) )
          | ( V_ba_2 = V_a_Ha_2 )
          | ( V_a_Ha_2 = V_b_Ha_2 )
          | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_P_Ha_2,c_Arrow__Order__Mirabelle_OProf)
          | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_Pa_2,c_Arrow__Order__Mirabelle_OProf)
          | ~ ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(V_Pa_2,tptp_fun_B_i_1(V_aa_2,V_ba_2,V_a_Ha_2,V_b_Ha_2,V_Pa_2,V_P_Ha_2)))
            <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(V_P_Ha_2,tptp_fun_B_i_1(V_aa_2,V_ba_2,V_a_Ha_2,V_b_Ha_2,V_Pa_2,V_P_Ha_2))) ) ) )),
    inference(bind,[status(th)],[]) ).

tff(9,plain,
    ( ! [V_P_Ha_2: $i,V_Pa_2: $i,V_b_Ha_2: $i,V_a_Ha_2: $i,V_ba_2: $i,V_aa_2: $i] :
        ( ( V_aa_2 = V_ba_2 )
        | ( V_aa_2 = V_b_Ha_2 )
        | ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(v_F,V_Pa_2))
        <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(v_F,V_P_Ha_2)) )
        | ( V_ba_2 = V_a_Ha_2 )
        | ( V_a_Ha_2 = V_b_Ha_2 )
        | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_P_Ha_2,c_Arrow__Order__Mirabelle_OProf)
        | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_Pa_2,c_Arrow__Order__Mirabelle_OProf)
        | ~ ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(V_Pa_2,tptp_fun_B_i_1(V_aa_2,V_ba_2,V_a_Ha_2,V_b_Ha_2,V_Pa_2,V_P_Ha_2)))
          <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(V_P_Ha_2,tptp_fun_B_i_1(V_aa_2,V_ba_2,V_a_Ha_2,V_b_Ha_2,V_Pa_2,V_P_Ha_2))) ) )
  <=> ! [V_P_Ha_2: $i,V_Pa_2: $i,V_b_Ha_2: $i,V_a_Ha_2: $i,V_ba_2: $i,V_aa_2: $i] :
        ( ( V_aa_2 = V_ba_2 )
        | ( V_aa_2 = V_b_Ha_2 )
        | ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(v_F,V_Pa_2))
        <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(v_F,V_P_Ha_2)) )
        | ( V_ba_2 = V_a_Ha_2 )
        | ( V_a_Ha_2 = V_b_Ha_2 )
        | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_P_Ha_2,c_Arrow__Order__Mirabelle_OProf)
        | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_Pa_2,c_Arrow__Order__Mirabelle_OProf)
        | ~ ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(V_Pa_2,tptp_fun_B_i_1(V_aa_2,V_ba_2,V_a_Ha_2,V_b_Ha_2,V_Pa_2,V_P_Ha_2)))
          <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(V_P_Ha_2,tptp_fun_B_i_1(V_aa_2,V_ba_2,V_a_Ha_2,V_b_Ha_2,V_Pa_2,V_P_Ha_2))) ) ) ),
    inference(quant_intro,[status(thm)],[8]) ).

tff(10,plain,
    ^ [V_P_Ha_2: $i,V_Pa_2: $i,V_b_Ha_2: $i,V_a_Ha_2: $i,V_ba_2: $i,V_aa_2: $i] :
      trans(monotonicity(rewrite(( ~ ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(V_Pa_2,tptp_fun_B_i_1(V_aa_2,V_ba_2,V_a_Ha_2,V_b_Ha_2,V_Pa_2,V_P_Ha_2)))
              <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(V_P_Ha_2,tptp_fun_B_i_1(V_aa_2,V_ba_2,V_a_Ha_2,V_b_Ha_2,V_Pa_2,V_P_Ha_2))) )
          <=> ~ ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(V_Pa_2,tptp_fun_B_i_1(V_aa_2,V_ba_2,V_a_Ha_2,V_b_Ha_2,V_Pa_2,V_P_Ha_2)))
              <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(V_P_Ha_2,tptp_fun_B_i_1(V_aa_2,V_ba_2,V_a_Ha_2,V_b_Ha_2,V_Pa_2,V_P_Ha_2))) ) )),
          ( ( ( V_aa_2 = V_ba_2 )
            | ( V_aa_2 = V_b_Ha_2 )
            | ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(v_F,V_Pa_2))
            <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(v_F,V_P_Ha_2)) )
            | ( V_ba_2 = V_a_Ha_2 )
            | ( V_a_Ha_2 = V_b_Ha_2 )
            | ~ ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(V_Pa_2,tptp_fun_B_i_1(V_aa_2,V_ba_2,V_a_Ha_2,V_b_Ha_2,V_Pa_2,V_P_Ha_2)))
              <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(V_P_Ha_2,tptp_fun_B_i_1(V_aa_2,V_ba_2,V_a_Ha_2,V_b_Ha_2,V_Pa_2,V_P_Ha_2))) )
            | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_P_Ha_2,c_Arrow__Order__Mirabelle_OProf)
            | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_Pa_2,c_Arrow__Order__Mirabelle_OProf) )
        <=> ( ( V_aa_2 = V_ba_2 )
            | ( V_aa_2 = V_b_Ha_2 )
            | ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(v_F,V_Pa_2))
            <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(v_F,V_P_Ha_2)) )
            | ( V_ba_2 = V_a_Ha_2 )
            | ( V_a_Ha_2 = V_b_Ha_2 )
            | ~ ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(V_Pa_2,tptp_fun_B_i_1(V_aa_2,V_ba_2,V_a_Ha_2,V_b_Ha_2,V_Pa_2,V_P_Ha_2)))
              <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(V_P_Ha_2,tptp_fun_B_i_1(V_aa_2,V_ba_2,V_a_Ha_2,V_b_Ha_2,V_Pa_2,V_P_Ha_2))) )
            | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_P_Ha_2,c_Arrow__Order__Mirabelle_OProf)
            | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_Pa_2,c_Arrow__Order__Mirabelle_OProf) ) )),
        rewrite(( ( ( V_aa_2 = V_ba_2 )
            | ( V_aa_2 = V_b_Ha_2 )
            | ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(v_F,V_Pa_2))
            <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(v_F,V_P_Ha_2)) )
            | ( V_ba_2 = V_a_Ha_2 )
            | ( V_a_Ha_2 = V_b_Ha_2 )
            | ~ ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(V_Pa_2,tptp_fun_B_i_1(V_aa_2,V_ba_2,V_a_Ha_2,V_b_Ha_2,V_Pa_2,V_P_Ha_2)))
              <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(V_P_Ha_2,tptp_fun_B_i_1(V_aa_2,V_ba_2,V_a_Ha_2,V_b_Ha_2,V_Pa_2,V_P_Ha_2))) )
            | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_P_Ha_2,c_Arrow__Order__Mirabelle_OProf)
            | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_Pa_2,c_Arrow__Order__Mirabelle_OProf) )
        <=> ( ( V_aa_2 = V_ba_2 )
            | ( V_aa_2 = V_b_Ha_2 )
            | ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(v_F,V_Pa_2))
            <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(v_F,V_P_Ha_2)) )
            | ( V_ba_2 = V_a_Ha_2 )
            | ( V_a_Ha_2 = V_b_Ha_2 )
            | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_P_Ha_2,c_Arrow__Order__Mirabelle_OProf)
            | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_Pa_2,c_Arrow__Order__Mirabelle_OProf)
            | ~ ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(V_Pa_2,tptp_fun_B_i_1(V_aa_2,V_ba_2,V_a_Ha_2,V_b_Ha_2,V_Pa_2,V_P_Ha_2)))
              <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(V_P_Ha_2,tptp_fun_B_i_1(V_aa_2,V_ba_2,V_a_Ha_2,V_b_Ha_2,V_Pa_2,V_P_Ha_2))) ) ) )),
        ( ( ( V_aa_2 = V_ba_2 )
          | ( V_aa_2 = V_b_Ha_2 )
          | ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(v_F,V_Pa_2))
          <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(v_F,V_P_Ha_2)) )
          | ( V_ba_2 = V_a_Ha_2 )
          | ( V_a_Ha_2 = V_b_Ha_2 )
          | ~ ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(V_Pa_2,tptp_fun_B_i_1(V_aa_2,V_ba_2,V_a_Ha_2,V_b_Ha_2,V_Pa_2,V_P_Ha_2)))
            <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(V_P_Ha_2,tptp_fun_B_i_1(V_aa_2,V_ba_2,V_a_Ha_2,V_b_Ha_2,V_Pa_2,V_P_Ha_2))) )
          | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_P_Ha_2,c_Arrow__Order__Mirabelle_OProf)
          | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_Pa_2,c_Arrow__Order__Mirabelle_OProf) )
      <=> ( ( V_aa_2 = V_ba_2 )
          | ( V_aa_2 = V_b_Ha_2 )
          | ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(v_F,V_Pa_2))
          <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(v_F,V_P_Ha_2)) )
          | ( V_ba_2 = V_a_Ha_2 )
          | ( V_a_Ha_2 = V_b_Ha_2 )
          | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_P_Ha_2,c_Arrow__Order__Mirabelle_OProf)
          | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_Pa_2,c_Arrow__Order__Mirabelle_OProf)
          | ~ ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(V_Pa_2,tptp_fun_B_i_1(V_aa_2,V_ba_2,V_a_Ha_2,V_b_Ha_2,V_Pa_2,V_P_Ha_2)))
            <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(V_P_Ha_2,tptp_fun_B_i_1(V_aa_2,V_ba_2,V_a_Ha_2,V_b_Ha_2,V_Pa_2,V_P_Ha_2))) ) ) )),
    inference(bind,[status(th)],[]) ).

tff(11,plain,
    ( ! [V_P_Ha_2: $i,V_Pa_2: $i,V_b_Ha_2: $i,V_a_Ha_2: $i,V_ba_2: $i,V_aa_2: $i] :
        ( ( V_aa_2 = V_ba_2 )
        | ( V_aa_2 = V_b_Ha_2 )
        | ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(v_F,V_Pa_2))
        <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(v_F,V_P_Ha_2)) )
        | ( V_ba_2 = V_a_Ha_2 )
        | ( V_a_Ha_2 = V_b_Ha_2 )
        | ~ ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(V_Pa_2,tptp_fun_B_i_1(V_aa_2,V_ba_2,V_a_Ha_2,V_b_Ha_2,V_Pa_2,V_P_Ha_2)))
          <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(V_P_Ha_2,tptp_fun_B_i_1(V_aa_2,V_ba_2,V_a_Ha_2,V_b_Ha_2,V_Pa_2,V_P_Ha_2))) )
        | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_P_Ha_2,c_Arrow__Order__Mirabelle_OProf)
        | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_Pa_2,c_Arrow__Order__Mirabelle_OProf) )
  <=> ! [V_P_Ha_2: $i,V_Pa_2: $i,V_b_Ha_2: $i,V_a_Ha_2: $i,V_ba_2: $i,V_aa_2: $i] :
        ( ( V_aa_2 = V_ba_2 )
        | ( V_aa_2 = V_b_Ha_2 )
        | ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(v_F,V_Pa_2))
        <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(v_F,V_P_Ha_2)) )
        | ( V_ba_2 = V_a_Ha_2 )
        | ( V_a_Ha_2 = V_b_Ha_2 )
        | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_P_Ha_2,c_Arrow__Order__Mirabelle_OProf)
        | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_Pa_2,c_Arrow__Order__Mirabelle_OProf)
        | ~ ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(V_Pa_2,tptp_fun_B_i_1(V_aa_2,V_ba_2,V_a_Ha_2,V_b_Ha_2,V_Pa_2,V_P_Ha_2)))
          <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(V_P_Ha_2,tptp_fun_B_i_1(V_aa_2,V_ba_2,V_a_Ha_2,V_b_Ha_2,V_Pa_2,V_P_Ha_2))) ) ) ),
    inference(quant_intro,[status(thm)],[10]) ).

tff(12,plain,
    ( ! [V_P_Ha_2: $i,V_Pa_2: $i,V_b_Ha_2: $i,V_a_Ha_2: $i,V_ba_2: $i,V_aa_2: $i] :
        ( ( V_aa_2 = V_ba_2 )
        | ( V_aa_2 = V_b_Ha_2 )
        | ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(v_F,V_Pa_2))
        <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(v_F,V_P_Ha_2)) )
        | ( V_ba_2 = V_a_Ha_2 )
        | ( V_a_Ha_2 = V_b_Ha_2 )
        | ~ ! [B_i: $i] :
              ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(V_Pa_2,B_i))
            <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(V_P_Ha_2,B_i)) )
        | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_P_Ha_2,c_Arrow__Order__Mirabelle_OProf)
        | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_Pa_2,c_Arrow__Order__Mirabelle_OProf) )
  <=> ! [V_P_Ha_2: $i,V_Pa_2: $i,V_b_Ha_2: $i,V_a_Ha_2: $i,V_ba_2: $i,V_aa_2: $i] :
        ( ( V_aa_2 = V_ba_2 )
        | ( V_aa_2 = V_b_Ha_2 )
        | ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(v_F,V_Pa_2))
        <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(v_F,V_P_Ha_2)) )
        | ( V_ba_2 = V_a_Ha_2 )
        | ( V_a_Ha_2 = V_b_Ha_2 )
        | ~ ! [B_i: $i] :
              ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(V_Pa_2,B_i))
            <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(V_P_Ha_2,B_i)) )
        | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_P_Ha_2,c_Arrow__Order__Mirabelle_OProf)
        | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_Pa_2,c_Arrow__Order__Mirabelle_OProf) ) ),
    inference(rewrite,[status(thm)],[]) ).

tff(13,plain,
    ^ [V_P_Ha_2: $i,V_Pa_2: $i,V_b_Ha_2: $i,V_a_Ha_2: $i,V_ba_2: $i,V_aa_2: $i] :
      trans(monotonicity(trans(monotonicity(trans(monotonicity(trans(monotonicity(trans(monotonicity(trans(monotonicity(rewrite(( ( ! [B_i: $i] :
                                      ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(V_Pa_2,B_i))
                                    <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(V_P_Ha_2,B_i)) )
                                 => ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(v_F,V_Pa_2))
                                  <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(v_F,V_P_Ha_2)) ) )
                              <=> ( ~ ! [B_i: $i] :
                                        ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(V_Pa_2,B_i))
                                      <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(V_P_Ha_2,B_i)) )
                                  | ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(v_F,V_Pa_2))
                                  <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(v_F,V_P_Ha_2)) ) ) )),
                              ( ( c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_P_Ha_2,c_Arrow__Order__Mirabelle_OProf)
                               => ( ! [B_i: $i] :
                                      ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(V_Pa_2,B_i))
                                    <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(V_P_Ha_2,B_i)) )
                                 => ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(v_F,V_Pa_2))
                                  <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(v_F,V_P_Ha_2)) ) ) )
                            <=> ( c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_P_Ha_2,c_Arrow__Order__Mirabelle_OProf)
                               => ( ~ ! [B_i: $i] :
                                        ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(V_Pa_2,B_i))
                                      <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(V_P_Ha_2,B_i)) )
                                  | ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(v_F,V_Pa_2))
                                  <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(v_F,V_P_Ha_2)) ) ) ) )),
                            rewrite(( ( c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_P_Ha_2,c_Arrow__Order__Mirabelle_OProf)
                               => ( ~ ! [B_i: $i] :
                                        ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(V_Pa_2,B_i))
                                      <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(V_P_Ha_2,B_i)) )
                                  | ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(v_F,V_Pa_2))
                                  <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(v_F,V_P_Ha_2)) ) ) )
                            <=> ( ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(v_F,V_Pa_2))
                                <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(v_F,V_P_Ha_2)) )
                                | ~ ! [B_i: $i] :
                                      ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(V_Pa_2,B_i))
                                    <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(V_P_Ha_2,B_i)) )
                                | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_P_Ha_2,c_Arrow__Order__Mirabelle_OProf) ) )),
                            ( ( c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_P_Ha_2,c_Arrow__Order__Mirabelle_OProf)
                             => ( ! [B_i: $i] :
                                    ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(V_Pa_2,B_i))
                                  <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(V_P_Ha_2,B_i)) )
                               => ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(v_F,V_Pa_2))
                                <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(v_F,V_P_Ha_2)) ) ) )
                          <=> ( ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(v_F,V_Pa_2))
                              <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(v_F,V_P_Ha_2)) )
                              | ~ ! [B_i: $i] :
                                    ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(V_Pa_2,B_i))
                                  <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(V_P_Ha_2,B_i)) )
                              | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_P_Ha_2,c_Arrow__Order__Mirabelle_OProf) ) )),
                          ( ( c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_Pa_2,c_Arrow__Order__Mirabelle_OProf)
                           => ( c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_P_Ha_2,c_Arrow__Order__Mirabelle_OProf)
                             => ( ! [B_i: $i] :
                                    ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(V_Pa_2,B_i))
                                  <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(V_P_Ha_2,B_i)) )
                               => ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(v_F,V_Pa_2))
                                <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(v_F,V_P_Ha_2)) ) ) ) )
                        <=> ( c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_Pa_2,c_Arrow__Order__Mirabelle_OProf)
                           => ( ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(v_F,V_Pa_2))
                              <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(v_F,V_P_Ha_2)) )
                              | ~ ! [B_i: $i] :
                                    ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(V_Pa_2,B_i))
                                  <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(V_P_Ha_2,B_i)) )
                              | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_P_Ha_2,c_Arrow__Order__Mirabelle_OProf) ) ) )),
                        rewrite(( ( c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_Pa_2,c_Arrow__Order__Mirabelle_OProf)
                           => ( ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(v_F,V_Pa_2))
                              <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(v_F,V_P_Ha_2)) )
                              | ~ ! [B_i: $i] :
                                    ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(V_Pa_2,B_i))
                                  <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(V_P_Ha_2,B_i)) )
                              | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_P_Ha_2,c_Arrow__Order__Mirabelle_OProf) ) )
                        <=> ( ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(v_F,V_Pa_2))
                            <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(v_F,V_P_Ha_2)) )
                            | ~ ! [B_i: $i] :
                                  ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(V_Pa_2,B_i))
                                <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(V_P_Ha_2,B_i)) )
                            | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_P_Ha_2,c_Arrow__Order__Mirabelle_OProf)
                            | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_Pa_2,c_Arrow__Order__Mirabelle_OProf) ) )),
                        ( ( c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_Pa_2,c_Arrow__Order__Mirabelle_OProf)
                         => ( c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_P_Ha_2,c_Arrow__Order__Mirabelle_OProf)
                           => ( ! [B_i: $i] :
                                  ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(V_Pa_2,B_i))
                                <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(V_P_Ha_2,B_i)) )
                             => ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(v_F,V_Pa_2))
                              <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(v_F,V_P_Ha_2)) ) ) ) )
                      <=> ( ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(v_F,V_Pa_2))
                          <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(v_F,V_P_Ha_2)) )
                          | ~ ! [B_i: $i] :
                                ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(V_Pa_2,B_i))
                              <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(V_P_Ha_2,B_i)) )
                          | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_P_Ha_2,c_Arrow__Order__Mirabelle_OProf)
                          | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_Pa_2,c_Arrow__Order__Mirabelle_OProf) ) )),
                      ( ( ( V_ba_2 != V_a_Ha_2 )
                       => ( c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_Pa_2,c_Arrow__Order__Mirabelle_OProf)
                         => ( c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_P_Ha_2,c_Arrow__Order__Mirabelle_OProf)
                           => ( ! [B_i: $i] :
                                  ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(V_Pa_2,B_i))
                                <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(V_P_Ha_2,B_i)) )
                             => ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(v_F,V_Pa_2))
                              <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(v_F,V_P_Ha_2)) ) ) ) ) )
                    <=> ( ( V_ba_2 != V_a_Ha_2 )
                       => ( ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(v_F,V_Pa_2))
                          <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(v_F,V_P_Ha_2)) )
                          | ~ ! [B_i: $i] :
                                ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(V_Pa_2,B_i))
                              <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(V_P_Ha_2,B_i)) )
                          | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_P_Ha_2,c_Arrow__Order__Mirabelle_OProf)
                          | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_Pa_2,c_Arrow__Order__Mirabelle_OProf) ) ) )),
                    rewrite(( ( ( V_ba_2 != V_a_Ha_2 )
                       => ( ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(v_F,V_Pa_2))
                          <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(v_F,V_P_Ha_2)) )
                          | ~ ! [B_i: $i] :
                                ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(V_Pa_2,B_i))
                              <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(V_P_Ha_2,B_i)) )
                          | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_P_Ha_2,c_Arrow__Order__Mirabelle_OProf)
                          | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_Pa_2,c_Arrow__Order__Mirabelle_OProf) ) )
                    <=> ( ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(v_F,V_Pa_2))
                        <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(v_F,V_P_Ha_2)) )
                        | ( V_ba_2 = V_a_Ha_2 )
                        | ~ ! [B_i: $i] :
                              ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(V_Pa_2,B_i))
                            <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(V_P_Ha_2,B_i)) )
                        | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_P_Ha_2,c_Arrow__Order__Mirabelle_OProf)
                        | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_Pa_2,c_Arrow__Order__Mirabelle_OProf) ) )),
                    ( ( ( V_ba_2 != V_a_Ha_2 )
                     => ( c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_Pa_2,c_Arrow__Order__Mirabelle_OProf)
                       => ( c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_P_Ha_2,c_Arrow__Order__Mirabelle_OProf)
                         => ( ! [B_i: $i] :
                                ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(V_Pa_2,B_i))
                              <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(V_P_Ha_2,B_i)) )
                           => ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(v_F,V_Pa_2))
                            <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(v_F,V_P_Ha_2)) ) ) ) ) )
                  <=> ( ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(v_F,V_Pa_2))
                      <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(v_F,V_P_Ha_2)) )
                      | ( V_ba_2 = V_a_Ha_2 )
                      | ~ ! [B_i: $i] :
                            ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(V_Pa_2,B_i))
                          <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(V_P_Ha_2,B_i)) )
                      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_P_Ha_2,c_Arrow__Order__Mirabelle_OProf)
                      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_Pa_2,c_Arrow__Order__Mirabelle_OProf) ) )),
                  ( ( ( V_aa_2 != V_b_Ha_2 )
                   => ( ( V_ba_2 != V_a_Ha_2 )
                     => ( c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_Pa_2,c_Arrow__Order__Mirabelle_OProf)
                       => ( c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_P_Ha_2,c_Arrow__Order__Mirabelle_OProf)
                         => ( ! [B_i: $i] :
                                ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(V_Pa_2,B_i))
                              <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(V_P_Ha_2,B_i)) )
                           => ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(v_F,V_Pa_2))
                            <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(v_F,V_P_Ha_2)) ) ) ) ) ) )
                <=> ( ( V_aa_2 != V_b_Ha_2 )
                   => ( ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(v_F,V_Pa_2))
                      <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(v_F,V_P_Ha_2)) )
                      | ( V_ba_2 = V_a_Ha_2 )
                      | ~ ! [B_i: $i] :
                            ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(V_Pa_2,B_i))
                          <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(V_P_Ha_2,B_i)) )
                      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_P_Ha_2,c_Arrow__Order__Mirabelle_OProf)
                      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_Pa_2,c_Arrow__Order__Mirabelle_OProf) ) ) )),
                rewrite(( ( ( V_aa_2 != V_b_Ha_2 )
                   => ( ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(v_F,V_Pa_2))
                      <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(v_F,V_P_Ha_2)) )
                      | ( V_ba_2 = V_a_Ha_2 )
                      | ~ ! [B_i: $i] :
                            ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(V_Pa_2,B_i))
                          <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(V_P_Ha_2,B_i)) )
                      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_P_Ha_2,c_Arrow__Order__Mirabelle_OProf)
                      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_Pa_2,c_Arrow__Order__Mirabelle_OProf) ) )
                <=> ( ( V_aa_2 = V_b_Ha_2 )
                    | ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(v_F,V_Pa_2))
                    <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(v_F,V_P_Ha_2)) )
                    | ( V_ba_2 = V_a_Ha_2 )
                    | ~ ! [B_i: $i] :
                          ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(V_Pa_2,B_i))
                        <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(V_P_Ha_2,B_i)) )
                    | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_P_Ha_2,c_Arrow__Order__Mirabelle_OProf)
                    | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_Pa_2,c_Arrow__Order__Mirabelle_OProf) ) )),
                ( ( ( V_aa_2 != V_b_Ha_2 )
                 => ( ( V_ba_2 != V_a_Ha_2 )
                   => ( c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_Pa_2,c_Arrow__Order__Mirabelle_OProf)
                     => ( c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_P_Ha_2,c_Arrow__Order__Mirabelle_OProf)
                       => ( ! [B_i: $i] :
                              ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(V_Pa_2,B_i))
                            <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(V_P_Ha_2,B_i)) )
                         => ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(v_F,V_Pa_2))
                          <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(v_F,V_P_Ha_2)) ) ) ) ) ) )
              <=> ( ( V_aa_2 = V_b_Ha_2 )
                  | ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(v_F,V_Pa_2))
                  <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(v_F,V_P_Ha_2)) )
                  | ( V_ba_2 = V_a_Ha_2 )
                  | ~ ! [B_i: $i] :
                        ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(V_Pa_2,B_i))
                      <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(V_P_Ha_2,B_i)) )
                  | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_P_Ha_2,c_Arrow__Order__Mirabelle_OProf)
                  | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_Pa_2,c_Arrow__Order__Mirabelle_OProf) ) )),
              ( ( ( V_a_Ha_2 != V_b_Ha_2 )
               => ( ( V_aa_2 != V_b_Ha_2 )
                 => ( ( V_ba_2 != V_a_Ha_2 )
                   => ( c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_Pa_2,c_Arrow__Order__Mirabelle_OProf)
                     => ( c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_P_Ha_2,c_Arrow__Order__Mirabelle_OProf)
                       => ( ! [B_i: $i] :
                              ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(V_Pa_2,B_i))
                            <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(V_P_Ha_2,B_i)) )
                         => ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(v_F,V_Pa_2))
                          <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(v_F,V_P_Ha_2)) ) ) ) ) ) ) )
            <=> ( ( V_a_Ha_2 != V_b_Ha_2 )
               => ( ( V_aa_2 = V_b_Ha_2 )
                  | ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(v_F,V_Pa_2))
                  <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(v_F,V_P_Ha_2)) )
                  | ( V_ba_2 = V_a_Ha_2 )
                  | ~ ! [B_i: $i] :
                        ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(V_Pa_2,B_i))
                      <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(V_P_Ha_2,B_i)) )
                  | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_P_Ha_2,c_Arrow__Order__Mirabelle_OProf)
                  | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_Pa_2,c_Arrow__Order__Mirabelle_OProf) ) ) )),
            rewrite(( ( ( V_a_Ha_2 != V_b_Ha_2 )
               => ( ( V_aa_2 = V_b_Ha_2 )
                  | ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(v_F,V_Pa_2))
                  <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(v_F,V_P_Ha_2)) )
                  | ( V_ba_2 = V_a_Ha_2 )
                  | ~ ! [B_i: $i] :
                        ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(V_Pa_2,B_i))
                      <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(V_P_Ha_2,B_i)) )
                  | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_P_Ha_2,c_Arrow__Order__Mirabelle_OProf)
                  | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_Pa_2,c_Arrow__Order__Mirabelle_OProf) ) )
            <=> ( ( V_aa_2 = V_b_Ha_2 )
                | ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(v_F,V_Pa_2))
                <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(v_F,V_P_Ha_2)) )
                | ( V_ba_2 = V_a_Ha_2 )
                | ( V_a_Ha_2 = V_b_Ha_2 )
                | ~ ! [B_i: $i] :
                      ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(V_Pa_2,B_i))
                    <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(V_P_Ha_2,B_i)) )
                | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_P_Ha_2,c_Arrow__Order__Mirabelle_OProf)
                | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_Pa_2,c_Arrow__Order__Mirabelle_OProf) ) )),
            ( ( ( V_a_Ha_2 != V_b_Ha_2 )
             => ( ( V_aa_2 != V_b_Ha_2 )
               => ( ( V_ba_2 != V_a_Ha_2 )
                 => ( c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_Pa_2,c_Arrow__Order__Mirabelle_OProf)
                   => ( c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_P_Ha_2,c_Arrow__Order__Mirabelle_OProf)
                     => ( ! [B_i: $i] :
                            ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(V_Pa_2,B_i))
                          <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(V_P_Ha_2,B_i)) )
                       => ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(v_F,V_Pa_2))
                        <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(v_F,V_P_Ha_2)) ) ) ) ) ) ) )
          <=> ( ( V_aa_2 = V_b_Ha_2 )
              | ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(v_F,V_Pa_2))
              <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(v_F,V_P_Ha_2)) )
              | ( V_ba_2 = V_a_Ha_2 )
              | ( V_a_Ha_2 = V_b_Ha_2 )
              | ~ ! [B_i: $i] :
                    ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(V_Pa_2,B_i))
                  <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(V_P_Ha_2,B_i)) )
              | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_P_Ha_2,c_Arrow__Order__Mirabelle_OProf)
              | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_Pa_2,c_Arrow__Order__Mirabelle_OProf) ) )),
          ( ( ( V_aa_2 != V_ba_2 )
           => ( ( V_a_Ha_2 != V_b_Ha_2 )
             => ( ( V_aa_2 != V_b_Ha_2 )
               => ( ( V_ba_2 != V_a_Ha_2 )
                 => ( c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_Pa_2,c_Arrow__Order__Mirabelle_OProf)
                   => ( c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_P_Ha_2,c_Arrow__Order__Mirabelle_OProf)
                     => ( ! [B_i: $i] :
                            ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(V_Pa_2,B_i))
                          <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(V_P_Ha_2,B_i)) )
                       => ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(v_F,V_Pa_2))
                        <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(v_F,V_P_Ha_2)) ) ) ) ) ) ) ) )
        <=> ( ( V_aa_2 != V_ba_2 )
           => ( ( V_aa_2 = V_b_Ha_2 )
              | ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(v_F,V_Pa_2))
              <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(v_F,V_P_Ha_2)) )
              | ( V_ba_2 = V_a_Ha_2 )
              | ( V_a_Ha_2 = V_b_Ha_2 )
              | ~ ! [B_i: $i] :
                    ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(V_Pa_2,B_i))
                  <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(V_P_Ha_2,B_i)) )
              | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_P_Ha_2,c_Arrow__Order__Mirabelle_OProf)
              | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_Pa_2,c_Arrow__Order__Mirabelle_OProf) ) ) )),
        rewrite(( ( ( V_aa_2 != V_ba_2 )
           => ( ( V_aa_2 = V_b_Ha_2 )
              | ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(v_F,V_Pa_2))
              <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(v_F,V_P_Ha_2)) )
              | ( V_ba_2 = V_a_Ha_2 )
              | ( V_a_Ha_2 = V_b_Ha_2 )
              | ~ ! [B_i: $i] :
                    ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(V_Pa_2,B_i))
                  <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(V_P_Ha_2,B_i)) )
              | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_P_Ha_2,c_Arrow__Order__Mirabelle_OProf)
              | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_Pa_2,c_Arrow__Order__Mirabelle_OProf) ) )
        <=> ( ( V_aa_2 = V_ba_2 )
            | ( V_aa_2 = V_b_Ha_2 )
            | ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(v_F,V_Pa_2))
            <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(v_F,V_P_Ha_2)) )
            | ( V_ba_2 = V_a_Ha_2 )
            | ( V_a_Ha_2 = V_b_Ha_2 )
            | ~ ! [B_i: $i] :
                  ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(V_Pa_2,B_i))
                <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(V_P_Ha_2,B_i)) )
            | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_P_Ha_2,c_Arrow__Order__Mirabelle_OProf)
            | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_Pa_2,c_Arrow__Order__Mirabelle_OProf) ) )),
        ( ( ( V_aa_2 != V_ba_2 )
         => ( ( V_a_Ha_2 != V_b_Ha_2 )
           => ( ( V_aa_2 != V_b_Ha_2 )
             => ( ( V_ba_2 != V_a_Ha_2 )
               => ( c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_Pa_2,c_Arrow__Order__Mirabelle_OProf)
                 => ( c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_P_Ha_2,c_Arrow__Order__Mirabelle_OProf)
                   => ( ! [B_i: $i] :
                          ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(V_Pa_2,B_i))
                        <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(V_P_Ha_2,B_i)) )
                     => ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(v_F,V_Pa_2))
                      <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(v_F,V_P_Ha_2)) ) ) ) ) ) ) ) )
      <=> ( ( V_aa_2 = V_ba_2 )
          | ( V_aa_2 = V_b_Ha_2 )
          | ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(v_F,V_Pa_2))
          <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(v_F,V_P_Ha_2)) )
          | ( V_ba_2 = V_a_Ha_2 )
          | ( V_a_Ha_2 = V_b_Ha_2 )
          | ~ ! [B_i: $i] :
                ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(V_Pa_2,B_i))
              <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(V_P_Ha_2,B_i)) )
          | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_P_Ha_2,c_Arrow__Order__Mirabelle_OProf)
          | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_Pa_2,c_Arrow__Order__Mirabelle_OProf) ) )),
    inference(bind,[status(th)],[]) ).

tff(14,plain,
    ( ! [V_P_Ha_2: $i,V_Pa_2: $i,V_b_Ha_2: $i,V_a_Ha_2: $i,V_ba_2: $i,V_aa_2: $i] :
        ( ( V_aa_2 != V_ba_2 )
       => ( ( V_a_Ha_2 != V_b_Ha_2 )
         => ( ( V_aa_2 != V_b_Ha_2 )
           => ( ( V_ba_2 != V_a_Ha_2 )
             => ( c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_Pa_2,c_Arrow__Order__Mirabelle_OProf)
               => ( c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_P_Ha_2,c_Arrow__Order__Mirabelle_OProf)
                 => ( ! [B_i: $i] :
                        ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(V_Pa_2,B_i))
                      <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(V_P_Ha_2,B_i)) )
                   => ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(v_F,V_Pa_2))
                    <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(v_F,V_P_Ha_2)) ) ) ) ) ) ) ) )
  <=> ! [V_P_Ha_2: $i,V_Pa_2: $i,V_b_Ha_2: $i,V_a_Ha_2: $i,V_ba_2: $i,V_aa_2: $i] :
        ( ( V_aa_2 = V_ba_2 )
        | ( V_aa_2 = V_b_Ha_2 )
        | ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(v_F,V_Pa_2))
        <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(v_F,V_P_Ha_2)) )
        | ( V_ba_2 = V_a_Ha_2 )
        | ( V_a_Ha_2 = V_b_Ha_2 )
        | ~ ! [B_i: $i] :
              ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(V_Pa_2,B_i))
            <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(V_P_Ha_2,B_i)) )
        | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_P_Ha_2,c_Arrow__Order__Mirabelle_OProf)
        | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_Pa_2,c_Arrow__Order__Mirabelle_OProf) ) ),
    inference(quant_intro,[status(thm)],[13]) ).

tff(15,axiom,
    ! [V_P_Ha_2: $i,V_Pa_2: $i,V_b_Ha_2: $i,V_a_Ha_2: $i,V_ba_2: $i,V_aa_2: $i] :
      ( ( V_aa_2 != V_ba_2 )
     => ( ( V_a_Ha_2 != V_b_Ha_2 )
       => ( ( V_aa_2 != V_b_Ha_2 )
         => ( ( V_ba_2 != V_a_Ha_2 )
           => ( c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_Pa_2,c_Arrow__Order__Mirabelle_OProf)
             => ( c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_P_Ha_2,c_Arrow__Order__Mirabelle_OProf)
               => ( ! [B_i: $i] :
                      ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(V_Pa_2,B_i))
                    <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(V_P_Ha_2,B_i)) )
                 => ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(v_F,V_Pa_2))
                  <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(v_F,V_P_Ha_2)) ) ) ) ) ) ) ) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact__C2_C) ).

tff(16,plain,
    ! [V_P_Ha_2: $i,V_Pa_2: $i,V_b_Ha_2: $i,V_a_Ha_2: $i,V_ba_2: $i,V_aa_2: $i] :
      ( ( V_aa_2 = V_ba_2 )
      | ( V_aa_2 = V_b_Ha_2 )
      | ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(v_F,V_Pa_2))
      <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(v_F,V_P_Ha_2)) )
      | ( V_ba_2 = V_a_Ha_2 )
      | ( V_a_Ha_2 = V_b_Ha_2 )
      | ~ ! [B_i: $i] :
            ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(V_Pa_2,B_i))
          <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(V_P_Ha_2,B_i)) )
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_P_Ha_2,c_Arrow__Order__Mirabelle_OProf)
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_Pa_2,c_Arrow__Order__Mirabelle_OProf) ),
    inference(modus_ponens,[status(thm)],[15,14]) ).

tff(17,plain,
    ! [V_P_Ha_2: $i,V_Pa_2: $i,V_b_Ha_2: $i,V_a_Ha_2: $i,V_ba_2: $i,V_aa_2: $i] :
      ( ( V_aa_2 = V_ba_2 )
      | ( V_aa_2 = V_b_Ha_2 )
      | ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(v_F,V_Pa_2))
      <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(v_F,V_P_Ha_2)) )
      | ( V_ba_2 = V_a_Ha_2 )
      | ( V_a_Ha_2 = V_b_Ha_2 )
      | ~ ! [B_i: $i] :
            ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(V_Pa_2,B_i))
          <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(V_P_Ha_2,B_i)) )
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_P_Ha_2,c_Arrow__Order__Mirabelle_OProf)
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_Pa_2,c_Arrow__Order__Mirabelle_OProf) ),
    inference(modus_ponens,[status(thm)],[16,12]) ).

tff(18,plain,
    ! [V_P_Ha_2: $i,V_Pa_2: $i,V_b_Ha_2: $i,V_a_Ha_2: $i,V_ba_2: $i,V_aa_2: $i] :
      ( ( V_aa_2 = V_ba_2 )
      | ( V_aa_2 = V_b_Ha_2 )
      | ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(v_F,V_Pa_2))
      <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(v_F,V_P_Ha_2)) )
      | ( V_ba_2 = V_a_Ha_2 )
      | ( V_a_Ha_2 = V_b_Ha_2 )
      | ~ ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(V_Pa_2,tptp_fun_B_i_1(V_aa_2,V_ba_2,V_a_Ha_2,V_b_Ha_2,V_Pa_2,V_P_Ha_2)))
        <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(V_P_Ha_2,tptp_fun_B_i_1(V_aa_2,V_ba_2,V_a_Ha_2,V_b_Ha_2,V_Pa_2,V_P_Ha_2))) )
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_P_Ha_2,c_Arrow__Order__Mirabelle_OProf)
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_Pa_2,c_Arrow__Order__Mirabelle_OProf) ),
    inference(skolemize,[status(sab)],[17]) ).

tff(19,plain,
    ! [V_P_Ha_2: $i,V_Pa_2: $i,V_b_Ha_2: $i,V_a_Ha_2: $i,V_ba_2: $i,V_aa_2: $i] :
      ( ( V_aa_2 = V_ba_2 )
      | ( V_aa_2 = V_b_Ha_2 )
      | ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(v_F,V_Pa_2))
      <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(v_F,V_P_Ha_2)) )
      | ( V_ba_2 = V_a_Ha_2 )
      | ( V_a_Ha_2 = V_b_Ha_2 )
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_P_Ha_2,c_Arrow__Order__Mirabelle_OProf)
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_Pa_2,c_Arrow__Order__Mirabelle_OProf)
      | ~ ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(V_Pa_2,tptp_fun_B_i_1(V_aa_2,V_ba_2,V_a_Ha_2,V_b_Ha_2,V_Pa_2,V_P_Ha_2)))
        <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(V_P_Ha_2,tptp_fun_B_i_1(V_aa_2,V_ba_2,V_a_Ha_2,V_b_Ha_2,V_Pa_2,V_P_Ha_2))) ) ),
    inference(modus_ponens,[status(thm)],[18,11]) ).

tff(20,plain,
    ! [V_P_Ha_2: $i,V_Pa_2: $i,V_b_Ha_2: $i,V_a_Ha_2: $i,V_ba_2: $i,V_aa_2: $i] :
      ( ( V_aa_2 = V_ba_2 )
      | ( V_aa_2 = V_b_Ha_2 )
      | ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(v_F,V_Pa_2))
      <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(v_F,V_P_Ha_2)) )
      | ( V_ba_2 = V_a_Ha_2 )
      | ( V_a_Ha_2 = V_b_Ha_2 )
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_P_Ha_2,c_Arrow__Order__Mirabelle_OProf)
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_Pa_2,c_Arrow__Order__Mirabelle_OProf)
      | ~ ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(V_Pa_2,tptp_fun_B_i_1(V_aa_2,V_ba_2,V_a_Ha_2,V_b_Ha_2,V_Pa_2,V_P_Ha_2)))
        <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(V_P_Ha_2,tptp_fun_B_i_1(V_aa_2,V_ba_2,V_a_Ha_2,V_b_Ha_2,V_Pa_2,V_P_Ha_2))) ) ),
    inference(modus_ponens,[status(thm)],[19,9]) ).

tff(21,plain,
    ( c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),v_P_H____,c_Arrow__Order__Mirabelle_OProf)
  <=> c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),v_P_H____,c_Arrow__Order__Mirabelle_OProf) ),
    inference(rewrite,[status(thm)],[]) ).

tff(22,axiom,
    c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),v_P_H____,c_Arrow__Order__Mirabelle_OProf),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_A_I4_J) ).

tff(23,plain,
    c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),v_P_H____,c_Arrow__Order__Mirabelle_OProf),
    inference(modus_ponens,[status(thm)],[22,21]) ).

tff(24,plain,
    ( c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),v_P____,c_Arrow__Order__Mirabelle_OProf)
  <=> c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),v_P____,c_Arrow__Order__Mirabelle_OProf) ),
    inference(rewrite,[status(thm)],[]) ).

tff(25,axiom,
    c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),v_P____,c_Arrow__Order__Mirabelle_OProf),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_A_I3_J) ).

tff(26,plain,
    c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),v_P____,c_Arrow__Order__Mirabelle_OProf),
    inference(modus_ponens,[status(thm)],[25,24]) ).

tff(27,plain,
    ( ( v_b____ != v_a_H____ )
  <=> ( v_b____ != v_a_H____ ) ),
    inference(rewrite,[status(thm)],[]) ).

tff(28,axiom,
    ( ( v_a____ != v_b_H____ )
    & ( v_b____ != v_a_H____ ) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact__096a_A_126_061_Ab_H_A_G_Ab_A_126_061_Aa_H_096) ).

tff(29,plain,
    v_b____ != v_a_H____,
    inference(and_elim,[status(thm)],[28]) ).

tff(30,plain,
    v_b____ != v_a_H____,
    inference(modus_ponens,[status(thm)],[29,27]) ).

tff(31,plain,
    ( ( v_a____ != v_b_H____ )
  <=> ( v_a____ != v_b_H____ ) ),
    inference(rewrite,[status(thm)],[]) ).

tff(32,plain,
    v_a____ != v_b_H____,
    inference(and_elim,[status(thm)],[28]) ).

tff(33,plain,
    v_a____ != v_b_H____,
    inference(modus_ponens,[status(thm)],[32,31]) ).

tff(34,plain,
    ( ( v_a_H____ != v_b_H____ )
  <=> ( v_a_H____ != v_b_H____ ) ),
    inference(rewrite,[status(thm)],[]) ).

tff(35,axiom,
    v_a_H____ != v_b_H____,
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_A_I2_J) ).

tff(36,plain,
    v_a_H____ != v_b_H____,
    inference(modus_ponens,[status(thm)],[35,34]) ).

tff(37,plain,
    ( ( v_a____ != v_b____ )
  <=> ( v_a____ != v_b____ ) ),
    inference(rewrite,[status(thm)],[]) ).

tff(38,axiom,
    v_a____ != v_b____,
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_A_I1_J) ).

tff(39,plain,
    v_a____ != v_b____,
    inference(modus_ponens,[status(thm)],[38,37]) ).

tff(40,plain,
    ( ( ~ ! [V_P_Ha_2: $i,V_Pa_2: $i,V_b_Ha_2: $i,V_a_Ha_2: $i,V_ba_2: $i,V_aa_2: $i] :
            ( ( V_aa_2 = V_ba_2 )
            | ( V_aa_2 = V_b_Ha_2 )
            | ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(v_F,V_Pa_2))
            <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(v_F,V_P_Ha_2)) )
            | ( V_ba_2 = V_a_Ha_2 )
            | ( V_a_Ha_2 = V_b_Ha_2 )
            | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_P_Ha_2,c_Arrow__Order__Mirabelle_OProf)
            | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_Pa_2,c_Arrow__Order__Mirabelle_OProf)
            | ~ ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(V_Pa_2,tptp_fun_B_i_1(V_aa_2,V_ba_2,V_a_Ha_2,V_b_Ha_2,V_Pa_2,V_P_Ha_2)))
              <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(V_P_Ha_2,tptp_fun_B_i_1(V_aa_2,V_ba_2,V_a_Ha_2,V_b_Ha_2,V_Pa_2,V_P_Ha_2))) ) )
      | ( v_a____ = v_b____ )
      | ( v_a_H____ = v_b_H____ )
      | ( v_a____ = v_b_H____ )
      | ( v_b____ = v_a_H____ )
      | ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a____,v_b____),hAPP(v_F,v_P____))
      <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(v_F,v_P_H____)) )
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),v_P____,c_Arrow__Order__Mirabelle_OProf)
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),v_P_H____,c_Arrow__Order__Mirabelle_OProf)
      | ~ ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a____,v_b____),hAPP(v_P____,tptp_fun_B_i_1(v_a____,v_b____,v_a_H____,v_b_H____,v_P____,v_P_H____)))
        <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(v_P_H____,tptp_fun_B_i_1(v_a____,v_b____,v_a_H____,v_b_H____,v_P____,v_P_H____))) ) )
  <=> ( ~ ! [V_P_Ha_2: $i,V_Pa_2: $i,V_b_Ha_2: $i,V_a_Ha_2: $i,V_ba_2: $i,V_aa_2: $i] :
            ( ( V_aa_2 = V_ba_2 )
            | ( V_aa_2 = V_b_Ha_2 )
            | ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(v_F,V_Pa_2))
            <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(v_F,V_P_Ha_2)) )
            | ( V_ba_2 = V_a_Ha_2 )
            | ( V_a_Ha_2 = V_b_Ha_2 )
            | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_P_Ha_2,c_Arrow__Order__Mirabelle_OProf)
            | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_Pa_2,c_Arrow__Order__Mirabelle_OProf)
            | ~ ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(V_Pa_2,tptp_fun_B_i_1(V_aa_2,V_ba_2,V_a_Ha_2,V_b_Ha_2,V_Pa_2,V_P_Ha_2)))
              <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(V_P_Ha_2,tptp_fun_B_i_1(V_aa_2,V_ba_2,V_a_Ha_2,V_b_Ha_2,V_Pa_2,V_P_Ha_2))) ) )
      | ( v_a____ = v_b____ )
      | ( v_a_H____ = v_b_H____ )
      | ( v_a____ = v_b_H____ )
      | ( v_b____ = v_a_H____ )
      | ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a____,v_b____),hAPP(v_F,v_P____))
      <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(v_F,v_P_H____)) )
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),v_P____,c_Arrow__Order__Mirabelle_OProf)
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),v_P_H____,c_Arrow__Order__Mirabelle_OProf)
      | ~ ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a____,v_b____),hAPP(v_P____,tptp_fun_B_i_1(v_a____,v_b____,v_a_H____,v_b_H____,v_P____,v_P_H____)))
        <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(v_P_H____,tptp_fun_B_i_1(v_a____,v_b____,v_a_H____,v_b_H____,v_P____,v_P_H____))) ) ) ),
    inference(rewrite,[status(thm)],[]) ).

tff(41,plain,
    ( ( ( v_a____ = v_b____ )
      | ( v_a____ = v_b_H____ )
      | ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a____,v_b____),hAPP(v_F,v_P____))
      <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(v_F,v_P_H____)) )
      | ( v_b____ = v_a_H____ )
      | ( v_a_H____ = v_b_H____ )
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),v_P_H____,c_Arrow__Order__Mirabelle_OProf)
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),v_P____,c_Arrow__Order__Mirabelle_OProf)
      | ~ ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a____,v_b____),hAPP(v_P____,tptp_fun_B_i_1(v_a____,v_b____,v_a_H____,v_b_H____,v_P____,v_P_H____)))
        <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(v_P_H____,tptp_fun_B_i_1(v_a____,v_b____,v_a_H____,v_b_H____,v_P____,v_P_H____))) ) )
  <=> ( ( v_a____ = v_b____ )
      | ( v_a_H____ = v_b_H____ )
      | ( v_a____ = v_b_H____ )
      | ( v_b____ = v_a_H____ )
      | ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a____,v_b____),hAPP(v_F,v_P____))
      <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(v_F,v_P_H____)) )
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),v_P____,c_Arrow__Order__Mirabelle_OProf)
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),v_P_H____,c_Arrow__Order__Mirabelle_OProf)
      | ~ ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a____,v_b____),hAPP(v_P____,tptp_fun_B_i_1(v_a____,v_b____,v_a_H____,v_b_H____,v_P____,v_P_H____)))
        <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(v_P_H____,tptp_fun_B_i_1(v_a____,v_b____,v_a_H____,v_b_H____,v_P____,v_P_H____))) ) ) ),
    inference(rewrite,[status(thm)],[]) ).

tff(42,plain,
    ( ~ ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a____,v_b____),hAPP(v_P____,tptp_fun_B_i_1(v_a____,v_b____,v_a_H____,v_b_H____,v_P____,v_P_H____)))
      <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(v_P_H____,tptp_fun_B_i_1(v_a____,v_b____,v_a_H____,v_b_H____,v_P____,v_P_H____))) )
  <=> ~ ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a____,v_b____),hAPP(v_P____,tptp_fun_B_i_1(v_a____,v_b____,v_a_H____,v_b_H____,v_P____,v_P_H____)))
      <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(v_P_H____,tptp_fun_B_i_1(v_a____,v_b____,v_a_H____,v_b_H____,v_P____,v_P_H____))) ) ),
    inference(rewrite,[status(thm)],[]) ).

tff(43,plain,
    ( ( ( v_a____ = v_b____ )
      | ( v_a____ = v_b_H____ )
      | ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a____,v_b____),hAPP(v_F,v_P____))
      <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(v_F,v_P_H____)) )
      | ( v_b____ = v_a_H____ )
      | ( v_a_H____ = v_b_H____ )
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),v_P_H____,c_Arrow__Order__Mirabelle_OProf)
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),v_P____,c_Arrow__Order__Mirabelle_OProf)
      | ~ ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a____,v_b____),hAPP(v_P____,tptp_fun_B_i_1(v_a____,v_b____,v_a_H____,v_b_H____,v_P____,v_P_H____)))
        <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(v_P_H____,tptp_fun_B_i_1(v_a____,v_b____,v_a_H____,v_b_H____,v_P____,v_P_H____))) ) )
  <=> ( ( v_a____ = v_b____ )
      | ( v_a____ = v_b_H____ )
      | ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a____,v_b____),hAPP(v_F,v_P____))
      <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(v_F,v_P_H____)) )
      | ( v_b____ = v_a_H____ )
      | ( v_a_H____ = v_b_H____ )
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),v_P_H____,c_Arrow__Order__Mirabelle_OProf)
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),v_P____,c_Arrow__Order__Mirabelle_OProf)
      | ~ ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a____,v_b____),hAPP(v_P____,tptp_fun_B_i_1(v_a____,v_b____,v_a_H____,v_b_H____,v_P____,v_P_H____)))
        <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(v_P_H____,tptp_fun_B_i_1(v_a____,v_b____,v_a_H____,v_b_H____,v_P____,v_P_H____))) ) ) ),
    inference(monotonicity,[status(thm)],[42]) ).

tff(44,plain,
    ( ( ( v_a____ = v_b____ )
      | ( v_a____ = v_b_H____ )
      | ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a____,v_b____),hAPP(v_F,v_P____))
      <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(v_F,v_P_H____)) )
      | ( v_b____ = v_a_H____ )
      | ( v_a_H____ = v_b_H____ )
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),v_P_H____,c_Arrow__Order__Mirabelle_OProf)
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),v_P____,c_Arrow__Order__Mirabelle_OProf)
      | ~ ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a____,v_b____),hAPP(v_P____,tptp_fun_B_i_1(v_a____,v_b____,v_a_H____,v_b_H____,v_P____,v_P_H____)))
        <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(v_P_H____,tptp_fun_B_i_1(v_a____,v_b____,v_a_H____,v_b_H____,v_P____,v_P_H____))) ) )
  <=> ( ( v_a____ = v_b____ )
      | ( v_a_H____ = v_b_H____ )
      | ( v_a____ = v_b_H____ )
      | ( v_b____ = v_a_H____ )
      | ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a____,v_b____),hAPP(v_F,v_P____))
      <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(v_F,v_P_H____)) )
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),v_P____,c_Arrow__Order__Mirabelle_OProf)
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),v_P_H____,c_Arrow__Order__Mirabelle_OProf)
      | ~ ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a____,v_b____),hAPP(v_P____,tptp_fun_B_i_1(v_a____,v_b____,v_a_H____,v_b_H____,v_P____,v_P_H____)))
        <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(v_P_H____,tptp_fun_B_i_1(v_a____,v_b____,v_a_H____,v_b_H____,v_P____,v_P_H____))) ) ) ),
    inference(transitivity,[status(thm)],[43,41]) ).

tff(45,plain,
    ( ( ~ ! [V_P_Ha_2: $i,V_Pa_2: $i,V_b_Ha_2: $i,V_a_Ha_2: $i,V_ba_2: $i,V_aa_2: $i] :
            ( ( V_aa_2 = V_ba_2 )
            | ( V_aa_2 = V_b_Ha_2 )
            | ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(v_F,V_Pa_2))
            <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(v_F,V_P_Ha_2)) )
            | ( V_ba_2 = V_a_Ha_2 )
            | ( V_a_Ha_2 = V_b_Ha_2 )
            | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_P_Ha_2,c_Arrow__Order__Mirabelle_OProf)
            | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_Pa_2,c_Arrow__Order__Mirabelle_OProf)
            | ~ ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(V_Pa_2,tptp_fun_B_i_1(V_aa_2,V_ba_2,V_a_Ha_2,V_b_Ha_2,V_Pa_2,V_P_Ha_2)))
              <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(V_P_Ha_2,tptp_fun_B_i_1(V_aa_2,V_ba_2,V_a_Ha_2,V_b_Ha_2,V_Pa_2,V_P_Ha_2))) ) )
      | ( v_a____ = v_b____ )
      | ( v_a____ = v_b_H____ )
      | ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a____,v_b____),hAPP(v_F,v_P____))
      <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(v_F,v_P_H____)) )
      | ( v_b____ = v_a_H____ )
      | ( v_a_H____ = v_b_H____ )
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),v_P_H____,c_Arrow__Order__Mirabelle_OProf)
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),v_P____,c_Arrow__Order__Mirabelle_OProf)
      | ~ ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a____,v_b____),hAPP(v_P____,tptp_fun_B_i_1(v_a____,v_b____,v_a_H____,v_b_H____,v_P____,v_P_H____)))
        <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(v_P_H____,tptp_fun_B_i_1(v_a____,v_b____,v_a_H____,v_b_H____,v_P____,v_P_H____))) ) )
  <=> ( ~ ! [V_P_Ha_2: $i,V_Pa_2: $i,V_b_Ha_2: $i,V_a_Ha_2: $i,V_ba_2: $i,V_aa_2: $i] :
            ( ( V_aa_2 = V_ba_2 )
            | ( V_aa_2 = V_b_Ha_2 )
            | ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(v_F,V_Pa_2))
            <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(v_F,V_P_Ha_2)) )
            | ( V_ba_2 = V_a_Ha_2 )
            | ( V_a_Ha_2 = V_b_Ha_2 )
            | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_P_Ha_2,c_Arrow__Order__Mirabelle_OProf)
            | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_Pa_2,c_Arrow__Order__Mirabelle_OProf)
            | ~ ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(V_Pa_2,tptp_fun_B_i_1(V_aa_2,V_ba_2,V_a_Ha_2,V_b_Ha_2,V_Pa_2,V_P_Ha_2)))
              <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(V_P_Ha_2,tptp_fun_B_i_1(V_aa_2,V_ba_2,V_a_Ha_2,V_b_Ha_2,V_Pa_2,V_P_Ha_2))) ) )
      | ( v_a____ = v_b____ )
      | ( v_a_H____ = v_b_H____ )
      | ( v_a____ = v_b_H____ )
      | ( v_b____ = v_a_H____ )
      | ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a____,v_b____),hAPP(v_F,v_P____))
      <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(v_F,v_P_H____)) )
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),v_P____,c_Arrow__Order__Mirabelle_OProf)
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),v_P_H____,c_Arrow__Order__Mirabelle_OProf)
      | ~ ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a____,v_b____),hAPP(v_P____,tptp_fun_B_i_1(v_a____,v_b____,v_a_H____,v_b_H____,v_P____,v_P_H____)))
        <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(v_P_H____,tptp_fun_B_i_1(v_a____,v_b____,v_a_H____,v_b_H____,v_P____,v_P_H____))) ) ) ),
    inference(monotonicity,[status(thm)],[44]) ).

tff(46,plain,
    ( ( ~ ! [V_P_Ha_2: $i,V_Pa_2: $i,V_b_Ha_2: $i,V_a_Ha_2: $i,V_ba_2: $i,V_aa_2: $i] :
            ( ( V_aa_2 = V_ba_2 )
            | ( V_aa_2 = V_b_Ha_2 )
            | ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(v_F,V_Pa_2))
            <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(v_F,V_P_Ha_2)) )
            | ( V_ba_2 = V_a_Ha_2 )
            | ( V_a_Ha_2 = V_b_Ha_2 )
            | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_P_Ha_2,c_Arrow__Order__Mirabelle_OProf)
            | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_Pa_2,c_Arrow__Order__Mirabelle_OProf)
            | ~ ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(V_Pa_2,tptp_fun_B_i_1(V_aa_2,V_ba_2,V_a_Ha_2,V_b_Ha_2,V_Pa_2,V_P_Ha_2)))
              <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(V_P_Ha_2,tptp_fun_B_i_1(V_aa_2,V_ba_2,V_a_Ha_2,V_b_Ha_2,V_Pa_2,V_P_Ha_2))) ) )
      | ( v_a____ = v_b____ )
      | ( v_a____ = v_b_H____ )
      | ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a____,v_b____),hAPP(v_F,v_P____))
      <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(v_F,v_P_H____)) )
      | ( v_b____ = v_a_H____ )
      | ( v_a_H____ = v_b_H____ )
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),v_P_H____,c_Arrow__Order__Mirabelle_OProf)
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),v_P____,c_Arrow__Order__Mirabelle_OProf)
      | ~ ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a____,v_b____),hAPP(v_P____,tptp_fun_B_i_1(v_a____,v_b____,v_a_H____,v_b_H____,v_P____,v_P_H____)))
        <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(v_P_H____,tptp_fun_B_i_1(v_a____,v_b____,v_a_H____,v_b_H____,v_P____,v_P_H____))) ) )
  <=> ( ~ ! [V_P_Ha_2: $i,V_Pa_2: $i,V_b_Ha_2: $i,V_a_Ha_2: $i,V_ba_2: $i,V_aa_2: $i] :
            ( ( V_aa_2 = V_ba_2 )
            | ( V_aa_2 = V_b_Ha_2 )
            | ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(v_F,V_Pa_2))
            <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(v_F,V_P_Ha_2)) )
            | ( V_ba_2 = V_a_Ha_2 )
            | ( V_a_Ha_2 = V_b_Ha_2 )
            | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_P_Ha_2,c_Arrow__Order__Mirabelle_OProf)
            | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_Pa_2,c_Arrow__Order__Mirabelle_OProf)
            | ~ ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(V_Pa_2,tptp_fun_B_i_1(V_aa_2,V_ba_2,V_a_Ha_2,V_b_Ha_2,V_Pa_2,V_P_Ha_2)))
              <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(V_P_Ha_2,tptp_fun_B_i_1(V_aa_2,V_ba_2,V_a_Ha_2,V_b_Ha_2,V_Pa_2,V_P_Ha_2))) ) )
      | ( v_a____ = v_b____ )
      | ( v_a_H____ = v_b_H____ )
      | ( v_a____ = v_b_H____ )
      | ( v_b____ = v_a_H____ )
      | ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a____,v_b____),hAPP(v_F,v_P____))
      <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(v_F,v_P_H____)) )
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),v_P____,c_Arrow__Order__Mirabelle_OProf)
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),v_P_H____,c_Arrow__Order__Mirabelle_OProf)
      | ~ ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a____,v_b____),hAPP(v_P____,tptp_fun_B_i_1(v_a____,v_b____,v_a_H____,v_b_H____,v_P____,v_P_H____)))
        <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(v_P_H____,tptp_fun_B_i_1(v_a____,v_b____,v_a_H____,v_b_H____,v_P____,v_P_H____))) ) ) ),
    inference(transitivity,[status(thm)],[45,40]) ).

tff(47,plain,
    ( ~ ! [V_P_Ha_2: $i,V_Pa_2: $i,V_b_Ha_2: $i,V_a_Ha_2: $i,V_ba_2: $i,V_aa_2: $i] :
          ( ( V_aa_2 = V_ba_2 )
          | ( V_aa_2 = V_b_Ha_2 )
          | ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(v_F,V_Pa_2))
          <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(v_F,V_P_Ha_2)) )
          | ( V_ba_2 = V_a_Ha_2 )
          | ( V_a_Ha_2 = V_b_Ha_2 )
          | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_P_Ha_2,c_Arrow__Order__Mirabelle_OProf)
          | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_Pa_2,c_Arrow__Order__Mirabelle_OProf)
          | ~ ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(V_Pa_2,tptp_fun_B_i_1(V_aa_2,V_ba_2,V_a_Ha_2,V_b_Ha_2,V_Pa_2,V_P_Ha_2)))
            <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(V_P_Ha_2,tptp_fun_B_i_1(V_aa_2,V_ba_2,V_a_Ha_2,V_b_Ha_2,V_Pa_2,V_P_Ha_2))) ) )
    | ( v_a____ = v_b____ )
    | ( v_a____ = v_b_H____ )
    | ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a____,v_b____),hAPP(v_F,v_P____))
    <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(v_F,v_P_H____)) )
    | ( v_b____ = v_a_H____ )
    | ( v_a_H____ = v_b_H____ )
    | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),v_P_H____,c_Arrow__Order__Mirabelle_OProf)
    | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),v_P____,c_Arrow__Order__Mirabelle_OProf)
    | ~ ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a____,v_b____),hAPP(v_P____,tptp_fun_B_i_1(v_a____,v_b____,v_a_H____,v_b_H____,v_P____,v_P_H____)))
      <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(v_P_H____,tptp_fun_B_i_1(v_a____,v_b____,v_a_H____,v_b_H____,v_P____,v_P_H____))) ) ),
    inference(quant_inst,[status(thm)],[]) ).

tff(48,plain,
    ( ~ ! [V_P_Ha_2: $i,V_Pa_2: $i,V_b_Ha_2: $i,V_a_Ha_2: $i,V_ba_2: $i,V_aa_2: $i] :
          ( ( V_aa_2 = V_ba_2 )
          | ( V_aa_2 = V_b_Ha_2 )
          | ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(v_F,V_Pa_2))
          <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(v_F,V_P_Ha_2)) )
          | ( V_ba_2 = V_a_Ha_2 )
          | ( V_a_Ha_2 = V_b_Ha_2 )
          | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_P_Ha_2,c_Arrow__Order__Mirabelle_OProf)
          | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),V_Pa_2,c_Arrow__Order__Mirabelle_OProf)
          | ~ ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(V_Pa_2,tptp_fun_B_i_1(V_aa_2,V_ba_2,V_a_Ha_2,V_b_Ha_2,V_Pa_2,V_P_Ha_2)))
            <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(V_P_Ha_2,tptp_fun_B_i_1(V_aa_2,V_ba_2,V_a_Ha_2,V_b_Ha_2,V_Pa_2,V_P_Ha_2))) ) )
    | ( v_a____ = v_b____ )
    | ( v_a_H____ = v_b_H____ )
    | ( v_a____ = v_b_H____ )
    | ( v_b____ = v_a_H____ )
    | ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a____,v_b____),hAPP(v_F,v_P____))
    <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(v_F,v_P_H____)) )
    | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),v_P____,c_Arrow__Order__Mirabelle_OProf)
    | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),v_P_H____,c_Arrow__Order__Mirabelle_OProf)
    | ~ ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a____,v_b____),hAPP(v_P____,tptp_fun_B_i_1(v_a____,v_b____,v_a_H____,v_b_H____,v_P____,v_P_H____)))
      <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(v_P_H____,tptp_fun_B_i_1(v_a____,v_b____,v_a_H____,v_b_H____,v_P____,v_P_H____))) ) ),
    inference(modus_ponens,[status(thm)],[47,46]) ).

tff(49,plain,
    ~ ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a____,v_b____),hAPP(v_P____,tptp_fun_B_i_1(v_a____,v_b____,v_a_H____,v_b_H____,v_P____,v_P_H____)))
    <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(v_P_H____,tptp_fun_B_i_1(v_a____,v_b____,v_a_H____,v_b_H____,v_P____,v_P_H____))) ),
    inference(unit_resolution,[status(thm)],[48,39,36,33,30,26,23,20,7]) ).

tff(50,plain,
    ^ [B_i: $i] :
      refl(( ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a____,v_b____),hAPP(v_P____,B_i))
        <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(v_P_H____,B_i)) )
      <=> ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a____,v_b____),hAPP(v_P____,B_i))
        <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(v_P_H____,B_i)) ) )),
    inference(bind,[status(th)],[]) ).

tff(51,plain,
    ( ! [B_i: $i] :
        ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a____,v_b____),hAPP(v_P____,B_i))
      <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(v_P_H____,B_i)) )
  <=> ! [B_i: $i] :
        ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a____,v_b____),hAPP(v_P____,B_i))
      <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(v_P_H____,B_i)) ) ),
    inference(quant_intro,[status(thm)],[50]) ).

tff(52,plain,
    ( ! [B_i: $i] :
        ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a____,v_b____),hAPP(v_P____,B_i))
      <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(v_P_H____,B_i)) )
  <=> ! [B_i: $i] :
        ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a____,v_b____),hAPP(v_P____,B_i))
      <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(v_P_H____,B_i)) ) ),
    inference(rewrite,[status(thm)],[]) ).

tff(53,axiom,
    ! [B_i: $i] :
      ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a____,v_b____),hAPP(v_P____,B_i))
    <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(v_P_H____,B_i)) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_A_I5_J) ).

tff(54,plain,
    ! [B_i: $i] :
      ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a____,v_b____),hAPP(v_P____,B_i))
    <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(v_P_H____,B_i)) ),
    inference(modus_ponens,[status(thm)],[53,52]) ).

tff(55,plain,
    ! [B_i: $i] :
      ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a____,v_b____),hAPP(v_P____,B_i))
    <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(v_P_H____,B_i)) ),
    inference(skolemize,[status(sab)],[54]) ).

tff(56,plain,
    ! [B_i: $i] :
      ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a____,v_b____),hAPP(v_P____,B_i))
    <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(v_P_H____,B_i)) ),
    inference(modus_ponens,[status(thm)],[55,51]) ).

tff(57,plain,
    ( ~ ! [B_i: $i] :
          ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a____,v_b____),hAPP(v_P____,B_i))
        <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(v_P_H____,B_i)) )
    | ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a____,v_b____),hAPP(v_P____,tptp_fun_B_i_1(v_a____,v_b____,v_a_H____,v_b_H____,v_P____,v_P_H____)))
    <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(v_P_H____,tptp_fun_B_i_1(v_a____,v_b____,v_a_H____,v_b_H____,v_P____,v_P_H____))) ) ),
    inference(quant_inst,[status(thm)],[]) ).

tff(58,plain,
    $false,
    inference(unit_resolution,[status(thm)],[57,56,49]) ).

%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.12  % Problem    : SCT155+1 : TPTP v9.0.0. Released v5.2.0.
% 0.12/0.12  % Command    : run_E %s %d THM
% 0.12/0.34  % Computer : n009.cluster.edu
% 0.12/0.34  % Model    : x86_64 x86_64
% 0.12/0.34  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34  % Memory   : 8042.1875MB
% 0.12/0.34  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34  % CPULimit   : 300
% 0.12/0.34  % WCLimit    : 300
% 0.12/0.34  % DateTime   : Fri Jun 20 03:51:33 EDT 2025
% 0.12/0.34  % CPUTime    : 
% 0.41/0.58  % SZS status Theorem
% 0.41/0.58  % SZS output start Proof
% See solution above
% 0.48/0.65  % E exiting
%------------------------------------------------------------------------------