proposition: Lemma synth_no_confusion : forall (si : state) (a : ast) (c : command) (e : perror), synthesis_trans si a c -> synth_error si a e -> False.
proof: Proof. simple induction 1; intros. inversion_clear H1. apply H4. apply equiv_no_undef with (glob_names si) t e0; auto with coc core arith datatypes. inversion_clear H2; auto with coc core arith datatypes. inversion_clear H2. apply H5. generalize H0 H1. inversion_clear H3; intros. apply equiv_no_undef with (glob_names si) m e0; auto with coc core arith datatypes. apply equiv_no_undef with (glob_names si) t e0; auto with coc core arith datatypes. inversion_clear H1. apply H4. apply equiv_no_undef with (glob_names si) t e0; auto with coc core arith datatypes. inversion_clear H2; auto with coc core arith datatypes. inversion_clear H0. inversion_clear H1. inversion_clear H0. inversion_clear H1. inversion_clear H0. inversion_clear H1. Qed.
imports: Termes Conv Types Conv_Dec Infer Expr