proposition: Lemma inverse_transport : SysF_INH (GammaH, poly_var tt) -> H10C_SAT h10cs.
proof: Proof. move=> [M] /typing_of_type_assignment [P] [_] {M}. move=> /typing_normal_form [{}P] [/construct_h10cs_solution] H /H{H}. apply. - constructor. { exists 0, 0, 0. do 3 (constructor; first by apply: encodes_natI). done. } constructor. { exists 1, 0, 1. do 3 (constructor; first by apply: encodes_natI). done. } constructor. { exists 0, 1, 1. do 3 (constructor; first by apply: encodes_natI). done. } done. - constructor. { exists 0, 0, 0. do 3 (constructor; first by apply: encodes_natI). done. } constructor. { exists 1, 0, 0. do 3 (constructor; first by apply: encodes_natI). done. } done. Qed.
imports: PeanoNat List Lia Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Util(Facts poly_type_facts term_facts typing_facts iipc2_facts sn_facts) Undecidability.DiophantineConstraints.H10C ssreflect ssrbool ssrfun