proposition: Lemma varL_exp (sigmaexp : fin -> exp ) : funcomp (subst_exp sigmaexp) (var_exp ) = sigmaexp .
proof: Proof. exact (FunctionalExtensionality.functional_extensionality _ _ (fun x => eq_refl)). Qed.
imports: Undecidability.HOU(std.std)