logic THF.THFP

spec test =

thf(type_a_1,type,( a_1 : $tType )).

thf(type_a_2_1,type,( a_2_1 : $tType )).

thf(type_a_2_2_1,type,( a_2_2_1 : $tType )).

thf(type_a_2_2_2,type,( a_2_2_2 : $tType )).

thf(type_c,type,( c : $tType )).

thf(test_const,type,( test_const : c > (a_1 > (a_2_1 * (a_2_2_1 * a_2_2_2))) )).

thf(test_tuple,type,( test_tuple : c )).

thf(const_b,type,( b : a_1 )).

thf(th,conjecture,( (pr_2 @ ((test_const @ test_tuple) @ b)) = (pr_2 @ ((test_const @ test_tuple) @ b)) )).