proposition: Lemma asimpl_scons_up_f B (f : nat -> B) : (f 0 .: (S >> f)) ≡ f.
proof: Proof. now intros [|n]. Qed.
imports: Undecidability.FOL.Syntax(Core Facts) Coq.Classes.Init Relation_Definitions Coq.Classes.RelationClasses Coq.Classes.Morphisms Setoid