proposition: Lemma finst_equivalence u v I W delta: I ⊆ nats (length W) -> AppR (ren delta (finst I (length W))) (Enc u v W) ≡ enc u v (concat (select I W)) (var (delta 0)).
proof: Proof. intros. unfold finst. rewrite !Lambda_ren, !AppL_ren. rewrite !map_id_list. 2: intros ? ?; mapinj; cbn; eapply H, nats_lt in H2; now rewrite it_up_ren_lt. cbn; rewrite it_up_ren_ge; (eauto 2); simplify. rewrite !AppR_Lambda'; simplify; (eauto 2). asimpl. rewrite !sapp_ge_in; simplify; (eauto 2). rewrite !select_variables_subst; [|simplify; (eauto 2)..]. now rewrite <-!select_map, enc_concat. Qed.
imports: RelationClasses Morphisms List Lia Arith Lia Init.Nat Setoid Undecidability.HOU(std.std calculus.calculus third_order.pcp)