proposition: Lemma append_const {A : Type} (a : A) (n1 n2 : nat) : append (const a n1) (const a n2) = const a (n1 + n2).
proof: Proof. induction n1. - reflexivity. - simpl. apply ap. assumption. Qed.
imports: Coq(ssreflect) HoTT(HoTT) HoTT_additions Hierarchy Param_nat