proposition: Lemma scons_eta f n : f n .: (+S n) >>> f = (+n) >>> f.
proof: Proof. f_ext; intros [|m]; simpl; [now rewrite plusnO|now rewrite plusnS]. Qed.
imports: Coq.Program.Tactics Coq.Arith.PeanoNat List FunctionalExtensionality