proposition: Lemma comp_assoc_simpl_comp {a} {tys : Vector.t obj_pair a} {dom mid cod} (f : Term tys mid cod) (g : Term tys dom mid) : comp_assoc_simpl (Comp f g) = match comp_assoc_simpl f in Term _ mid cod return Term tys dom mid -> Term tys dom cod with | Comp f f' => fun g => Comp f (comp_assoc_simpl (Comp f' g)) | x => fun g => Comp x (comp_assoc_simpl g) end g.
proof: Proof. unfold comp_assoc_simpl. simp comp_assoc_simpl_rec. revert dom g. Tactics.reverse. let felim := constr:(fun_elim (f := @comp_assoc_simpl_rec)) in unshelve refine_ho (felim _ _ _ _ _ _); simpl; intros; try reflexivity. Qed.
imports: Coq.Vectors.Vector Coq.PArith.PArith Lia Equations.Prop.Equations Wellfounded Relations