proposition: Lemma comp_assoc_simpl_ident {a} {tys : Vector.t obj_pair a} {dom cod} (g : Term tys dom cod) : comp_assoc_simpl (Comp Ident g) = Comp Ident (comp_assoc_simpl g).
proof: Proof. unfold comp_assoc_simpl. Opaque comp_assoc_simpl_rec. autorewrite with comp_assoc_simpl_rec. simpl. reflexivity. Qed.
imports: Coq.Vectors.Vector Coq.PArith.PArith Lia Equations.Prop.Equations Wellfounded Relations