proposition: Lemma decidable_tree : forall t, { convert_tree t } + { not (convert_tree t) }.
proof: Proof. induction t as [| |a|t Ht|t1 Ht1 t2 Ht2|t1 Ht1 t2 Ht2|t1 Ht1 t2 Ht2]. now left. now right. apply decidable_atom. destruct Ht as [Ht|Ht]. now right. now left. destruct Ht1 as [Ht1|Ht1]. destruct Ht2 as [Ht2|Ht2]. now left ; split. right. now intros (_,H). right. now intros (H,_). destruct Ht1 as [Ht1|Ht1]. left. now left. destruct Ht2 as [Ht2|Ht2]. left. now right. right. now intros [H|H]. destruct Ht2 as [Ht2|Ht2]. left. now intros _. destruct Ht1 as [Ht1|Ht1]. right. contradict Ht2. now apply Ht2. left. now intros H. Qed.
imports: Coq(ZArith Reals List Lia) Flocq(Core) Gappa_library