(A : Type) : Susp A -> Join Bool A. Proof. srapply (Susp_rec (joinl true) (joinl false)). intros a. exact (jglue _ a @ (jglue _ a)^). Defined.
Require Import Basics Types. Require Import Join.Core Join.JoinAssoc Suspension Spaces.Spheres. Require Import WildCat. Require Import Spaces.Nat.Core.