comparable → comparable → comparable.
#T1; #T2; napply (mk_comparable (ProdT T1 T2));
##[ napply (pair … (zeroc T1) (zeroc T2))
- ##| napply (λx.false)
+ ##| napply (λP.(forallc T1)
+ (λe1.(forallc T2)
+ (λe2.P (pair … e1 e2))))
##| napply (eq_pair … (eqc T1) (eqc T2))
##| napply (eqpair_to_eq … (eqc T1) (eqc T2));
##[ napply (eqc_to_eq T1)
comparable → comparable → comparable → comparable.
#T1; #T2; #T3; napply (mk_comparable (Prod3T T1 T2 T3));
##[ napply (triple … (zeroc T1) (zeroc T2) (zeroc T3))
- ##| napply (λx.false)
+ ##| napply (λP.(forallc T1)
+ (λe1.(forallc T2)
+ (λe2.(forallc T3)
+ (λe3.P (triple … e1 e2 e3)))))
##| napply (eq_triple … (eqc T1) (eqc T2) (eqc T3))
##| napply (eqtriple_to_eq … (eqc T1) (eqc T2) (eqc T3));
##[ napply (eqc_to_eq T1)
comparable → comparable → comparable → comparable → comparable.
#T1; #T2; #T3; #T4; napply (mk_comparable (Prod4T T1 T2 T3 T4));
##[ napply (quadruple … (zeroc T1) (zeroc T2) (zeroc T3) (zeroc T4))
- ##| napply (λx.false)
+ ##| napply (λP.(forallc T1)
+ (λe1.(forallc T2)
+ (λe2.(forallc T3)
+ (λe3.(forallc T4)
+ (λe4.P (quadruple … e1 e2 e3 e4))))))
##| napply (eq_quadruple … (eqc T1) (eqc T2) (eqc T3) (eqc T4))
##| napply (eqquadruple_to_eq … (eqc T1) (eqc T2) (eqc T3) (eqc T4));
##[ napply (eqc_to_eq T1)
comparable → comparable → comparable → comparable → comparable → comparable.
#T1; #T2; #T3; #T4; #T5; napply (mk_comparable (Prod5T T1 T2 T3 T4 T5));
##[ napply (quintuple … (zeroc T1) (zeroc T2) (zeroc T3) (zeroc T4) (zeroc T5))
- ##| napply (λx.false)
+ ##| napply (λP.(forallc T1)
+ (λe1.(forallc T2)
+ (λe2.(forallc T3)
+ (λe3.(forallc T4)
+ (λe4.(forallc T5)
+ (λe5.P (quintuple … e1 e2 e3 e4 e5)))))))
##| napply (eq_quintuple … (eqc T1) (eqc T2) (eqc T3) (eqc T4) (eqc T5))
##| napply (eqquintuple_to_eq … (eqc T1) (eqc T2) (eqc T3) (eqc T4) (eqc T5));
##[ napply (eqc_to_eq T1)