proposition: Lemma rinstInst_exp (xiexp : fin -> fin ) : ren_exp xiexp = subst_exp (funcomp (var_exp ) xiexp) .
proof: Proof. exact (FunctionalExtensionality.functional_extensionality _ _ (fun x => rinst_inst_exp xiexp (_) (fun n => eq_refl) x)). Qed.
imports: Undecidability.HOU(std.std)