proposition: Lemma app_strext: (bin_fun_strext free_csetoid_as_csetoid free_csetoid_as_csetoid free_csetoid_as_csetoid appA).
proof: Proof. unfold bin_fun_strext. intros x1. induction x1. simpl. intro x2. case x2. simpl. intuition. intuition. intros x2 y1 y2. simpl. case x2. case y2. simpl. intuition. simpl. intuition. case y2. simpl. simpl in IHx1. intros c l H. elim H. intuition. clear H. generalize (IHx1 l y1 (@nil A)). intuition. simpl. intros c l c0 l0. intro H. elim H. intuition. generalize (IHx1 l0 y1 (cons c l)). intuition. Qed.
imports: CoRN.algebra.CSetoids