{A} {B:A->Type} {f f' f'' : forall x, B x} (h:f=f') (h':f'=f'') (x:A) : apD10 (h @ h') x = apD10 h x @ apD10 h' x. Proof. case h, h'; reflexivity. Defined.
Require Import Basics.Overture Basics.Tactics.