proposition: Lemma type_assignment_allfv_substE Gamma1 Gamma2 M N s phi t : allfv (Nat.iter (length Gamma1) (scons True) is_nonzero) M -> type_assignment (Gamma1 ++ Gamma2) (subst (Nat.iter (length Gamma1) (fun sigma => scons (var 0) (fun x => ren S (sigma x))) (scons N var)) M) t -> type_assignment (Gamma1 ++ (s, phi) :: Gamma2) M t.
proof: Proof. move=> HM /(type_assignment_ren_fv _ (Gamma1 ++ (s, phi) :: Gamma2) (fun n => match (length Gamma1) - n with 0 => S n | _ => n end)). rewrite !simpl_term. have : forall (A B C : Prop), A -> (B -> C) -> (A -> B) -> C by auto. apply. { apply: allfv_subst. apply: allfv_impl HM. elim: (Gamma1). - by move=> [|x] /=. - move=> ?? IH [|x] /=; [done|]. move=> /IH H'. apply: allfv_ren. apply: allfv_impl H'. move=> x' /= {}IH > /IH <-. by case: (_ - _). } congr type_assignment. rewrite -[RHS]subst_var_term. apply: ext_allfv_subst_term. apply: allfv_impl HM. elim: (length Gamma1). { by case. } move=> x IH [|?] /=; [done|]. move=> /IH. rewrite !simpl_term /=. move: (Nat.iter _ _ _ _) => [? []|??|?] /=; [|done..]. move=> <-. congr var. by case: (_ - _). Qed.
imports: Undecidability.IntersectionTypes.CD Undecidability.IntersectionTypes.Util.CD_facts Undecidability.LambdaCalculus.Util.term_facts PeanoNat Relations List Lia ssreflect