proposition: Lemma contains_leftmost_path_length_eq {n s t} : contains (many_poly_abs n s) t -> not (is_poly_abs s) -> match leftmost_poly_var s with | None => leftmost_path_length s = leftmost_path_length t | Some x => n <= x -> leftmost_path_length s = leftmost_path_length t end.
proof: Proof. move Es': (many_poly_abs n s) => s' /clos_rt_rt1n_iff Hs't. elim: Hs't n s Es'. - move=> > <- _. rewrite ?leftmost_path_length_many_poly_abs. by case: (leftmost_poly_var _). - move=> > [] r > _ IH [|n]; first by case=> /=. move=> s [?]. subst. evar (s'' : poly_type). have := IH n s''. rewrite subst_poly_type_many_poly_abs. subst s'' => /(_ ltac:(done)). move: s {IH} => [x | s {}t | /=]; last done. + move=> /= + _ ?. have ->: x = n + (1 + (x - n - 1)) by lia. rewrite ?iter_up_poly_type_poly_type ?leftmost_poly_var_ren_poly_type ?leftmost_path_length_ren_poly_type /=. apply; by [|lia]. + move=> /(_ ltac:(done)). rewrite leftmost_poly_var_subst_poly_type /=. move Eox: (leftmost_poly_var s) => ox. case: ox Eox. * move=> x Hsx /= + _ ?. rewrite leftmost_path_length_subst_poly_type Hsx. have ->: x = n + (1 + (x - n - 1)) by lia. rewrite ?iter_up_poly_type_poly_type ?leftmost_poly_var_ren_poly_type ?leftmost_path_length_ren_poly_type /=. apply. by lia. * move=> /= Hs <- _. by rewrite leftmost_path_length_subst_poly_type Hs. Qed.
imports: List Lia Relation_Definitions Relation_Operators Operators_Properties Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.Util(Facts poly_type_facts pure_term_facts term_facts typing_facts iipc2_facts pure_typing_facts) ssreflect ssrbool ssrfun