proposition: Lemma ginst_equivalence I (S: stack): I <> nil -> I ⊆ nats (length S) -> AppR (ren (add 3) (finst I (length S))) (repeat (var (u 1)) (| S |)) ≡ var (u 1) (ren (add 3) (ginst I) (var (u 1))).
proof: Proof. intros H H0. unfold finst. rewrite !Lambda_ren, !AppL_ren. rewrite !map_id_list. 2: intros ? ?; mapinj; cbn; eapply H0, nats_lt in H3; now rewrite it_up_ren_lt. rewrite AppR_Lambda'; simplify; (auto 2). unfold ginst; cbn [ren]; rewrite stepBeta. 2: asimpl; simplify; cbn; unfold funcomp; (auto 2). cbn [ren]. rewrite it_up_ren_ge; simplify; (auto 2). asimpl. rewrite select_variables_subst; simplify; (auto 2). rewrite select_repeated; (auto 2). unfold ginst; cbn; asimpl; simplify. rewrite sapp_ge_in; simplify; (auto 3). replace (_ - _) with 3 by lia. destruct I; easy. Qed.
imports: RelationClasses Morphisms List Arith Lia Init.Nat Setoid Undecidability.HOU(std.std calculus.calculus unification.unification) Undecidability.HOU(third_order.pcp third_order.encoding)