proposition: Theorem phi_of_psi_succ : forall a b1 b2 n, phi a (gcons b1 b2 0 (fin (S n))) = if lt_ge_dec a b1 then [a, (gcons b1 b2 0 (fin n))] else [a ,(gcons b1 b2 0 (fin (S n)))].
proof: Proof. cbn; intros;case (lt_ge_dec a b1). - intro H; rewrite compare_rw_lt; auto with T2. - destruct 1. + subst b1; rewrite compare_rw_eq;auto with T2. + rewrite compare_rw_gt;auto with T2. Qed.
imports: Coq(Arith List Lia Compare_dec Relations Wellfounded RelationClasses) hydras(Epsilon0) hydras(More_Arith Restriction) hydras(ON_Generic) hydras(rpo.term rpo.rpo) hydras(T2) hydras(Compat815)