Library tactics_axioms

Require Export arity.

Class Col_theory (COLTpoint : Type) (CTCol: COLTpoint → COLTpoint → COLTpoint → Prop) :=
{
  CTcol_trivial : ∀ A B : COLTpoint, CTCol A A B;
  CTcol_permutation_1 : ∀ A B C : COLTpoint, CTCol A B C → CTCol B C A;
  CTcol_permutation_2 : ∀ A B C : COLTpoint, CTCol A B C → CTCol A C B;
  CTcol3 : ∀ X Y A B C : COLTpoint,
             X ≠ Y → CTCol X Y A → CTCol X Y B → CTCol X Y C → CTCol A B C
}.

Class Arity :=
{
  COATpoint : Type;
  n : nat
}.

Class Coapp_predicates (Ar : Arity) :=
{
  wd : arity COATpoint (S (S n));
  coapp : arity COATpoint (S (S (S n)))
}.

Class Coapp_theory (Ar : Arity) (COP : Coapp_predicates Ar) :=
{
  wd_perm_1 : ∀ A : COATpoint,
              ∀ X : cartesianPower COATpoint (S n),
                app_1_n wd A X → app_n_1 wd X A;
  wd_perm_2 : ∀ A B : COATpoint,
              ∀ X : cartesianPower COATpoint n,
                app_2_n wd A B X → app_2_n wd B A X;
  coapp_perm_1 : ∀ A : COATpoint,
                 ∀ X : cartesianPower COATpoint (S (S n)),
                   app_1_n coapp A X → app_n_1 coapp X A;
  coapp_perm_2 : ∀ A B : COATpoint,
                 ∀ X : cartesianPower COATpoint (S n),
                   app_2_n coapp A B X → app_2_n coapp B A X;
  link_betwenn_wd_and_coapp : ∀ A : COATpoint,
                              ∀ X : cartesianPower COATpoint (S (S n)),
                                app_1_n coapp A X ∨ app wd X;
  pseudo_trans_of_coapp : ∀ A B C : COATpoint,
                          ∀ X : cartesianPower COATpoint (S n),
                            app_1_n wd A X →
                            app_2_n coapp B A X →
                            app_2_n coapp C A X →
                            app_2_n coapp B C X
}.