proposition: Lemma subst_tt_fresh : forall Z U T, Z `notin` fv_tt T -> T = subst_tt Z U T.
proof: Proof. Proof with auto. induction T; simpl; intro H; f_equal... Case "typ_fvar". destruct (a == Z)... contradict H; fsetdec. Qed.
imports: Fsub.Fsub_LetSum_Definitions